Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CADE
2011
Springer
9 years 4 months ago
Extending Sledgehammer with SMT Solvers
Abstract. Sledgehammer is a component of Isabelle/HOL that employs firstorder automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically s...
Jasmin Christian Blanchette, Sascha Böhme, La...
VSTTE
2010
Springer
10 years 2 months ago
To Goto Where No Statement Has Gone Before
Abstract. This paper presents a method for deriving an expression from the lowlevel code compiled from an expression in a high-level language. The input is a low-level control flo...
Michael Barnett, K. Rustan M. Leino
books