• VeriFast

  • Referenced in 57 articles [sw07705]
  • safety properties of pointer-manipulating 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 proof-obligation 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 code-based paradigm ... using probabilistic programs. It provides a set of programming language tools (observational equivalence, relational Hoare...
  • KAT-ML

  • 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 while-language without threads, our proof shows that typeability in the Volpano/Smith system guarantees ... program execution are low-equivalent, then the final states are low-equivalent as well. This ... ports. The proof defines an abstract syntax and operational semantics for programs, formalizes noninterference...
  • LoPSiL

  • Referenced in 4 articles [sw02068]
  • mobile-device applications. We have implemented a proof-of-concept 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 alternation-free portion of guarded fixed ... results are complemented by inexpressibility proofs to the effect that linear-time 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 capture-avoiding substitution seem simple, yet subtle bugs ... implement the EDSL succinctly using datatype-generic programming. Our implementation supports a number of features...
  • VeriStar

  • Referenced in 3 articles [sw09393]
  • machine-checked, 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 ... plug-compatible 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 high-level 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...
  • HR-SQL

  • 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 Java-like 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...