• Isabelle/HOL

  • Referenced in 1017 articles [sw01569]
  • tools for proving those formulas in a logical calculus. The main application is the formalization ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...
  • Isabelle

  • Referenced in 713 articles [sw00454]
  • tools for proving those formulas in a logical calculus. The main application is the formalization ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...
  • KeYmaera

  • Referenced in 44 articles [sw03709]
  • prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic ... logic for hybrid programs, a program notation for hybrid automata. For automating the verification process...
  • HOL Light

  • Referenced in 308 articles [sw06580]
  • clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof ... formalization of mathematics and industrial formal verification...
  • ABC

  • Referenced in 40 articles [sw12910]
  • logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs ... combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative ... synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper...
  • JPAX

  • Referenced in 30 articles [sw09906]
  • overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX ... user provided properties formulated in temporal logic. JPAX can in addition analyze the program ... specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race...
  • Why3

  • Referenced in 135 articles [sw04438]
  • discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real ... used as an intermediate language for the verification of C, Java, or Ada programs. Why3...
  • VeriFast

  • Referenced in 64 articles [sw07705]
  • describes a separation-logic-based approach for the specification and verification of safety properties ... Verification proceeds by symbolic execution using an abstract representation of memory as a separation logic ... either the verifier or the SMT solver, verification time is predictable...
  • HIP

  • Referenced in 29 articles [sw09786]
  • programs. HIP is a separation logic based automated verification system for a simple imperative language ... will construct a set of separation logic proof obligations in the form of formula implications...
  • CESAR

  • Referenced in 161 articles [sw08510]
  • Specification and verification of concurrent systems in CESAR. The aim of this paper ... formulas of a branching time logic, the temporal operators of which can be computed iteratively ... fixed points of monotonic predicate transformers. The verification of a system consists in obtaining...
  • MCMAS

  • Referenced in 82 articles [sw09463]
  • Checker for the Verification of Multi-Agent Systems. While temporal logic in its various forms...
  • PPL

  • Referenced in 101 articles [sw05357]
  • verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous...
  • OBJ3

  • Referenced in 140 articles [sw05370]
  • proof system based on order sorted equational logic. It has been successfully used for research ... theorem proving, user interface design, and hardware verification, among other things. It was the first...
  • HANNIBAL

  • Referenced in 8 articles [sw10071]
  • HANNIBAL: An efficient tool for logic verification based on recursive learning. This paper introduces ... approach to logic verification of combinational circuits, which is based on recursive learning. In particular...
  • MCMAS-SLK

  • Referenced in 19 articles [sw24778]
  • model checker for the verification of strategy logic specifications. We introduce MCMAS ... verification of systems against specifications expressed in a novel, epistemic variant of strategy logic...
  • CVC

  • Referenced in 49 articles [sw09462]
  • logics and logical theories have proven to be useful tools in verification. This paper describes ... combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories...
  • TLPVS

  • Referenced in 10 articles [sw10024]
  • implementation of a linear temporal logic verification system. The system includes a set of theories ... defining a temporal logic, a number of proof rules for proving soundness and response properties ... system. A distributed rank rule for the verification of response properties in parameterized systems...
  • Viper

  • Referenced in 12 articles [sw15038]
  • reasoning. The automation of verification techniques based on first-order logic specifications has benefitted greatly ... well suited to verification techniques based on separation logic and other permission logics, because they ... existing tools for these logics often favour symbolic execution over verification condition generation. Consequently, tool ... support for these logics (where available) is typically developed independently for each technique, dramatically increasing...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • Boogie is a program verification condition generator for an imperative core language. It has front ... enriched by annotations in first-order logic.\parIts verification conditions -- constructed via a wp calculus...
  • ARMC

  • Referenced in 28 articles [sw04949]
  • Using a Prolog system together with Constraint Logic Programming extensions as the implementation platform ... which has already been used for practical verification...