• Boogie

  • Referenced in 118 articles [sw07714]
  • Boogie: An Intermediate Verification Language. Boogie is an intermediate verification language, intended as a layer...
  • Why3

  • Referenced in 130 articles [sw04438]
  • deductive program verification. It provides a rich language for specification and programming, called WhyML ... WhyML is also used as an intermediate language for the verification of C, Java...
  • CIL

  • Referenced in 36 articles [sw26691]
  • intermediate language and tools for analysis and transformation of C programs. This paper describes ... Intermediate Language: a highlevel representation along with a set of tools that permit easy analysis ... also more high-level than typical intermediate languages (e.g., three-address code) designed for compilation...
  • IF-2.0

  • Referenced in 46 articles [sw03303]
  • toolbox was built upon an intermediate representation language based on extended timed automata. In particular ... toolbox contains dedicated tools on the intermediate language (such as compilers, static analysers and model ... well as front-ends to various specification languages and validation tools (academic and commercial ones ... context: par -- the static nature of the intermediate representation prevents the analysis of dynamic systems...
  • VerICS

  • Referenced in 33 articles [sw02011]
  • written in a subset of the specification language Estelle, developed as a part ... specification, a specification in our original intermediate language (IL), or Timed Automata in the Kronos...
  • DACTL

  • Referenced in 28 articles [sw02871]
  • with Dactl, an associated compiler target (intermediate) language. An illustration of the capability of graph...
  • WhyML

  • Referenced in 25 articles [sw09709]
  • specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive ... WhyML is also used as an intermediate language for the verification of C, Java...
  • KITTeL

  • Referenced in 8 articles [sw17045]
  • analysis of C programs using compiler intermediate languages. Modeling the semantics of programming languages like ... other hand, low-level intermediate languages that occur during the compilation of C programs ... promising approach to use these intermediate languages for the automated termination analysis of C programs ... this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs...
  • SeaHorn

  • Referenced in 14 articles [sw18274]
  • concerns of the syntax of the programming language, its operational semantics, and the verification semantics ... uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with...
  • BoogiePL

  • Referenced in 12 articles [sw21521]
  • programs. This note defines BoogiePL, an intermediate language for program analysis and program verification...
  • Viper

  • Referenced in 8 articles [sw15038]
  • Boogie and Why. These offer an intermediate language that can express diverse language features ... present a verification infrastructure whose intermediate language supports an expressive permission model natively. We provide...
  • SymDiff

  • Referenced in 16 articles [sw13093]
  • this paper, we describe SymDiff, a language-agnostic tool for equivalence checking and displaying semantic ... programs. The tool operates on an intermediate verification language Boogie, for which translations exist from...
  • OFMC

  • Referenced in 27 articles [sw09466]
  • OFMC). The native input language of OFMC is the AVISPA Intermediate Format IF. OFMC also...
  • Pilsner

  • Referenced in 6 articles [sw20004]
  • verified compiler for a higher-order imperative language. Compiler verification is essential for the construction ... applicable to compilers that use different intermediate languages or employ non-standard program transformations ... going through a CPS-based intermediate language. Pilsner is the first multi-pass compiler...
  • GCminor

  • Referenced in 4 articles [sw22622]
  • certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor ... used with a wide variety of source languages and collector styles. Front ends targeting GCminor ... Glasgow Haskell Compiler’s Core intermediate language to GCminor. To support a simple but useful...
  • BAP

  • Referenced in 7 articles [sw12790]
  • side effects of instructions in an intermediate language (IL), making syntaxdirected analysis possible. We have...
  • Bedrock

  • Referenced in 4 articles [sw28530]
  • characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally ... saying that C is a ”macro assembly language”: we introduce an expressive notion of certified ... programs that compute programs in our intermediate language; but the run-time cost...
  • Fiacre

  • Referenced in 6 articles [sw07004]
  • Fiacre: an intermediate language for model verification in the topcased environment...
  • PolyAML

  • Referenced in 4 articles [sw08950]
  • translation into an expressive type-safe intermediate language. Many complexities of the source language ... novelties of the intermediate language is the definition of polymorphic labels for marking control-flow...
  • Bio-PEPA

  • Referenced in 104 articles [sw01361]
  • PEPA may be seen as an intermediate, formal, compositional representation of biological systems, on which ... PEPA have been considered andextended to our language. Finally, we show the translation...