Integrated reasoning and proof choice point selection in the jahob system (Mechanisms for program survival) by Rinard, Martin C.

“…In recent years researchers have developed a wide range of powerful automated reasoning systems. We have leveraged these systems to build Jahob, a program specification, analysis, and verification system. …”
Get full text
Get full text

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs by Pit-Claudel, Clement Francois, Wang, Peng, Delaware, Benjamin, Gross, Jason S., Chlipala, Adam

Get full text

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs by Pit-Claudel, Clément, Wang, Peng, Delaware, Benjamin, Gross, Jason S., Chlipala, Adam

Get full text

An Integrated Proof Language for Imperative Programs by Zee, Karen, Kuncak, Viktor, Rinard, Martin C.

“…Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems.…”
Get full text
Get full text

Polite Combination of Algebraic Datatypes by Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Lange, Jane, Fontaine, Pascal, Barrett, Clark

“…Abstract Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). …”
Get full text