- Referenced in 413 articles
- integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These...
- Referenced in 113 articles
- Why3 is a platform for deductive program verification. It provides a rich language for specification ... programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge ... verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic ... intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete...
- Referenced in 105 articles
- intermediate verification language, intended as a layer on which to build program verifiers for other ... languages. Several program verifiers have been built in this way, including the VCC and HAVOC ... name of the verification tool that takes Boogie programs as input. Boogie is also ... invariants in the given Boogie program, and then generates verification conditions that are passed...
- Referenced in 37 articles
- tool for solving semi-algebraic systems; Program Verification by Using DISCOVERER. Recent advances in program ... verification indicate that various verification problems can be reduced to semi-algebraic system ... problems. To overcome the bottleneck of program verification with a symbolic approach ... both on SAS-solving and program verification with DISCOVERER, and then discuss the future work...
- Referenced in 478 articles
- currying. It is used heavily in programming language research ... compiler writing, automated theorem proving and formal verification. (wikipedia...
- Referenced in 43 articles
- reachability analysis can be used for program verification. For instance, Timbuk is currently used...
- Referenced in 53 articles
- designed to support the static verification of programs. It is imperative, sequential, supports generic classes ... ghost constructs are used only during verification; the compiler omits them from the executable code.The ... errors, the programmer responds by changing the program’s type declarations, specifications, and statements...
- Referenced in 22 articles
- present Why3, a tool for deductive program verification, and WhyML, its programming and specification language ... polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with ... intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits ... WhyML on non-trivial examples of program verification...
- Referenced in 30 articles
- jStar: Towards practical verification for Java. In this paper we introduce a novel methodology ... verifying a large set of Java programs which ... builds on recent theoretical developments in program verification: it combines the idea of abstract predicate ... been implemented in a new automatic verification system, called jStar, which combines theorem proving...
- Referenced in 166 articles
- development of parallel and distributed programs -- as a platform for simulation model specification and analysis ... permitting formal verification of the transition systems, and second into an executable program are described...
- Referenced in 139 articles
- verification of a system consists in obtaining by automatic translation of its description program...
- Referenced in 115 articles
- verification tool for C language that solves the reachability problem, i.e. whether a given program ... point (main function) by a valid execution. Verification of safety properties may be reduced...
- Referenced in 38 articles
- HSolver is a program for verification of hybrid systems based on the constraint solver RSOLVER...
- Referenced in 63 articles
- Caduceus used to be a verification tool for C programs built...
- Referenced in 125 articles
- OBJ3 is a program specification and proof system based on order sorted equational logic ... hardware verification, among other things. It was the first language to implement parameterized programming...
- Referenced in 48 articles
- specification and verification of safety properties of pointer-manipulating imperative programs. The programmer may declare...
- Referenced in 16 articles
- programming language with effects aimed at program verification. It puts together the automation ... assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml...
- Referenced in 40 articles
- static debugging and verification, finding errors before running the program. This includes checking how programs...
- Referenced in 14 articles
- Boogie is a program verification condition generator for an imperative core language. It has front ... programming languages C# and C enriched by annotations in first-order logic.\parIts verification conditions...
- Referenced in 66 articles
- programming errors. We present our experience in performing the formal, machine-checked verification...