• z3

  • Referenced in 597 articles [sw04887]
  • functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification...
  • ML

  • Referenced in 522 articles [sw01218]
  • errors.[1] ML provides pattern matching for function arguments, garbage collection, imperative programming, call ... compiler writing, automated theorem proving and formal verification. (wikipedia...
  • BLAST

  • Referenced in 129 articles [sw02937]
  • Software verification Tool) is a static software verification tool for C language that solves ... entry point (main function) by a valid execution. Verification of safety properties may be reduced...
  • VeriFast

  • Referenced in 64 articles [sw07705]
  • logic-based approach for the specification and verification of safety properties of pointer-manipulating imperative ... inductive datatypes and primitive recursive functions for specification. Verification proceeds by symbolic execution using ... performed through explicit ghost statements. Lemma functions enable inductive proofs of memory representation equivalences ... facts about the primitive recursive functions. An SMT solver is used to solve queries over...
  • MathSAT

  • Referenced in 61 articles [sw09449]
  • useful theories: (combinations of) equality and uninterpreted functions, difference logic, linear arithmetic, and the theory ... being used in formal verification, and thus provides functionalities which extend the applicability...
  • Reveal

  • Referenced in 21 articles [sw00801]
  • describe the Reveal formal functional verification system and its application to four representative hardware test...
  • HIP

  • Referenced in 29 articles [sw09786]
  • HIP/SLEEK systems are aimed at automatic verification of functional correctness of heap manipulating programs...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • functional correctness of programs.The Dafny programming language is designed to support the static verification ... language also offers updatable ghost variables, recursive functions, and types like sets and sequences. Specifications ... ghost constructs are used only during verification; the compiler omits them from the executable code.The...
  • SLAM

  • Referenced in 153 articles [sw03136]
  • software that ensure reliable and correct functioning. Static Driver Verifier is a tool ... Driver Development Kit that uses the SLAM verification engine...
  • PPL

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

  • Referenced in 5 articles [sw30948]
  • AutoProof: Auto-active Functional Verification of Object-oriented Programs. Auto-active verifiers provide a level ... object-oriented sequential programs with complex functional specifications. AutoProof fully supports advanced object-oriented features ... league on cutting-edge functional verification of object-oriented programs...
  • Leon

  • Referenced in 11 articles [sw09159]
  • Leon verification system: verification by translation to recursive functions. We present the Leon verification system...
  • SpaceEx

  • Referenced in 75 articles [sw10939]
  • SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems ... deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute ... implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr...
  • SYMBA

  • Referenced in 13 articles [sw08528]
  • uses for them in software verification, program synthesis, functional programming, refinement types...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • state systems with variables of integer, Boolean, function, and array types. There are two main ... level bounded model checking, correspondence checking, deductive verification, and predicate abstraction ... based verification. As a stand-alone decision procedure for the theories of uninterpreted functions ... UCLID explored to-date include microprocessor design verification, analyzing software for security exploits, and verifying...
  • F*

  • Referenced in 20 articles [sw27563]
  • general-purpose functional programming language with effects aimed at program verification. It puts together ... proof assistant based on dependent types. After verification, F* programs can be extracted to efficient ... code. This enables verifying the functional correctness and security of realistic applications. The main ongoing...
  • FOCI

  • Referenced in 62 articles [sw12868]
  • certain interpreted theories, such as equality, uninterpreted functions, linear arithmetic, and arrays. Most importantly ... number of applications in infinite-state verification, for example, discovering predicates in predicate abstraction...
  • FunFrog

  • Referenced in 6 articles [sw06571]
  • function calls. In every successful verification run, FunFrog generates function summaries of the analyzed program ... functions and reuses them to reduce the complexity of the successive verification. To prevent reporting...
  • seL4

  • Referenced in 91 articles [sw15222]
  • experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract ... this is the first formal proof of functional correctness of a complete, general-purpose operating...
  • MAYA

  • Referenced in 26 articles [sw03423]
  • functionality will result in changes of the specification which always endangers the verification work already...