
VeriFast
 Referenced in 57 articles
[sw07705]
 safety properties of pointermanipulating imperative programs. The programmer may declare inductive datatypes and primitive ... statements. Lemma functions enable inductive proofs of memory representation equivalences and facts about the primitive...

Fiat
 Referenced in 14 articles
[sw21357]
 Fiat produces a formal proof trail certifying that the synthesized program meets the original specification ... Fiat can be extracted to an equivalent OCaml program that can be compiled...

IMP+Exc
 Referenced in 1 article
[sw28535]
 encoding is used to certify some program equivalence proofs...

TVOC
 Referenced in 19 articles
[sw02521]
 optimizations: for a given source program, TVOC proves the equivalence of the source code ... first phase verifies loop transformations using the proof rule permute; the second phase verifies structure...

EventB2Dafny
 Referenced in 2 articles
[sw16544]
 EventB machine proofobligation and generates an equivalent Dafny program. You can then use Dafny...

CertiCrypt
 Referenced in 6 articles
[sw09443]
 security of cryptographic primitives in the Coq proof assistant. CertiCrypt adopts the codebased paradigm ... using probabilistic programs. It provides a set of programming language tools (observational equivalence, relational Hoare...

KATML
 Referenced in 10 articles
[sw08506]
 reason about properties of simple imperative programs using schematic KAT (SKAT). We explain ... some examples, including an extensive scheme equivalence proof...

Volpano Smith
 Referenced in 1 article
[sw29543]
 simple whilelanguage without threads, our proof shows that typeability in the Volpano/Smith system guarantees ... program execution are lowequivalent, then the final states are lowequivalent as well. This ... ports. The proof defines an abstract syntax and operational semantics for programs, formalizes noninterference...

LoPSiL
 Referenced in 4 articles
[sw02068]
 mobiledevice applications. We have implemented a proofofconcept compiler that inputs a LoPSiL ... device application program A and outputs a new application program A ’ equivalent to A, except...

Datalog LITE
 Referenced in 10 articles
[sw28894]
 that is, linear time data complexity and program complexity. Datalog LITE is a variant ... Datalog LITE. Further, Datalog LITE is equivalent to the alternationfree portion of guarded fixed ... results are complemented by inexpressibility proofs to the effect that lineartime fragments of extit...

CoCLAM
 Referenced in 2 articles
[sw28719]
 exploits the information gained from the failed proof attempt. Our approach to the problem ... coinduction to prove the equivalence of programs in a small lazy functional language which ... similar to Haskell. We have developed a proof plan for coinduction and a critic associated...

Unbound
 Referenced in 4 articles
[sw22613]
 Binders unbound. mplementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that ... well. Operations such as αequivalence and captureavoiding substitution seem simple, yet subtle bugs ... implement the EDSL succinctly using datatypegeneric programming. Our implementation supports a number of features...

VeriStar
 Referenced in 3 articles
[sw09393]
 machinechecked, we mean it has a proof in Coq that when the prover says ... minor program is safe, the program will be compiled to a semantically equivalent assembly program ... plugcompatible entailment checker and its soundness proof can easily be ported to other separation...

XYZ/SE
 Referenced in 2 articles
[sw03027]
 system. A set of proof rules is given and proved to be sound and adequate ... XYZ/SE programs in a compositional way. Moreover, we show that every XYZ/BE program ... transformed into an equivalent XYZ/SE program. So we have developed a general compositional verification method...

F@BOOL@
 Referenced in 3 articles
[sw21004]
 from a highlevel language to equivalent executable programs and proves (verifies) mathematical statements specified ... human concerning the properties of the translated programs. The objective of the project F@BOOL ... portable verifying compiler of annotated computational programs that uses efficient and reliable automatic SAT solvers ... validation of correctness conditions (instead of semiautomatic proof techniques). In the period from...

HRSQL
 Referenced in 1 article
[sw32283]
 stratified fixpoint semantics based on logic programming techniques. We include results of the existence ... definitions into an equivalent one without hypothesis and its correctness proof are presented. Regarding...

Jinja not Java
 Referenced in 2 articles
[sw28876]
 Java We introduce Jinja, a Javalike programming language with a formal semantics designed ... semantics for Jinja and a proof of their equivalence; a type system and a definite...

ACL2
 Referenced in 281 articles
[sw00060]
 ACL2 is both a programming language in which...

CoCoA
 Referenced in 639 articles
[sw00143]
 CoCoA is a system for Computations in Commutative...

Coq
 Referenced in 1837 articles
[sw00161]
 Coq is a formal proof management system. It...