• ML

  • Referenced in 522 articles [sw01218]
  • such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • ghost constructs are used only during verification; the compiler omits them from the executable code.The...
  • CompCert

  • Referenced in 49 articles [sw09737]
  • CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such...
  • CakeML

  • Referenced in 53 articles [sw08799]
  • permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics ... lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler ... demonstrating that each piece of such a verification effort can in practice be composed with ... challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself...
  • Pilsner

  • Referenced in 6 articles [sw20004]
  • higher-order imperative language. Compiler verification is essential for the construction of fully verified software ... CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable ... develop a novel approach to compositional compiler verification based on parametric inter-language simulations (PILS ... PILS are modular: they enable compiler verification in a manner that supports separate compilation. PILS...
  • CAESAR

  • Referenced in 9 articles [sw29138]
  • caesar - compilation & verification of LOTOS specifications. caesar [Gar89b,GS90] is a compiler that translates ... this specification. caesar itself does not embody verification capabilities, but it smootly interfaces with many...
  • seL4

  • Referenced in 91 articles [sw15222]
  • experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract ... implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique...
  • CVT

  • Referenced in 16 articles [sw09952]
  • code validation tool (CVT). Automatic verification of a compilation process. We describe CVT -- a fully ... produced by a code-generator (equivalently, a compiler or a translator) is a correct implementation ... viable alternative to a full formal verification of the code-generator program...
  • Esterel

  • Referenced in 166 articles [sw20012]
  • systems and control automata. The Esterel v5 compiler can be used to generate a software ... provide support for explicit or BDD-based verification tools that perform either bisimulation reduction...
  • TVOC

  • Referenced in 20 articles [sw02521]
  • running the compiler. There are two phases to the verification process: the first phase verifies...
  • GROOVE

  • Referenced in 51 articles [sw09480]
  • GRaphs for Object-Oriented VErification (GROOVE). GROOVE is a project centered around ... simple graphs for modelling the design-time, compile-time, and run-time structure of object...
  • Sigma*

  • Referenced in 12 articles [sw21731]
  • useful for web sanitizer verification and stream programs compiler optimizations, as we show experimentally...
  • UFO

  • Referenced in 23 articles [sw09570]
  • Framework for Abstraction- and Interpolation-Based Software Verification. In this paper, we present ... LLVM compiler infrastructure and is targeted at researchers designing and experimenting with verification algorithms...
  • SMACK

  • Referenced in 9 articles [sw23311]
  • LLVM compiler’s popular intermediate representation (IR) into the Boogie intermediate verification language (IVL). Sourcing ... LLVM IR exploits an increasing number of compiler front-ends, optimizations, and analyses. Targeting Boogie ... which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation...
  • AnBx

  • Referenced in 3 articles [sw27775]
  • AnBx Compiler and Java Code Generator: Security Protocols Specification, Verification and Implementation - Alice ... Java Compiler. Features: AnBx to AnB compiler for verification (requires the OFMC model-checker); Java...
  • CoVaC

  • Referenced in 7 articles [sw21472]
  • CoVaC: compiler validation by program analysis of the cross-product. The paper presents a deductive ... application to automatic verification of transformations performed by optimizing compilers. To leverage existing program analysis...
  • LOOP

  • Referenced in 29 articles [sw10292]
  • LOOP compiler for Java and JML. This paper describes the architecture of the LOOP tool ... theorem prover in which the actual verification of the desired properties takes place. Also...
  • Joogie

  • Referenced in 4 articles [sw13771]
  • java through jimple to boogie. Recently, software verification is being used to prove the presence ... provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from...
  • Pinocchio

  • Referenced in 42 articles [sw10193]
  • first general-purpose system to demonstrate verification cheaper than native execution (for some apps). Pinocchio ... provides an end-to-end toolchain that compiles a subset of C into programs that...
  • LTSA-WS

  • Referenced in 14 articles [sw10585]
  • service implementations. The tool supports verification of properties created from design specifications and implementation models ... Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) process algebra ... allow an equivalence trace verification process to be performed. By providing early design verification...