RiSE Working Group on Program Analysis
The RiSE Working Group on Program Analysis (PAx) improves the productivity of developer and testers and the reliability and security of software systems via novel techniques and tools for program analysis, testing, and verification.
- Code DiggerCode Digger is a Microsoft® Visual Studio® 2012 extension that analyzes possible execution paths through your .NET code. The result is a table where each row shows a unique behavior of your code. The table helps you understand the behavior of the code, and it may also uncover hidden bugs.
- DualityDuality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such as automatic verification of sequential, concurrent and functional programs, as well as interactive refinement of manual proofs.
- Interpolating Z3Interpolating Z3 uses Z3's proof generation capability to generate Craig interpolants in the first-order theory of uninterpreted functions, arrays and linear arithmetic.
- F*: A Verifying ML Compiler for Distributed ProgrammingF* is a new dependently typed language for secure distributed programming. It's designed to be enable the construction and communication of proofs of program properties and of properties of a program's environment in a verifiably secure way. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based.
- SymDiff: Static semantic diffSymDiff (aka Symbolic Differencing) is an infrastructure for leveraging and extending program verification to reason about program changes. In a nutshell, Symdiff can be summarized as Windiff for behaviors. It builds up on recent advances on program equivalence checking using automated SMT solvers. However, it extends beyond program equivalence and deals with questions such as: (1) can one infer the conditions under which two programs are equivalent? (2) how do the changes affect the public API?
- Moles - Isolation framework for .NETMoles allows to replace any .NET method with a delegate. Moles supports static or non-virtual methods. Moles works well with Pex.
- Cuzz - Concurrency FuzzingCuzz is a very effective tool for finding concurrency bugs. Cuzz works on unmodified executables and is designed for maximizing concurrency coverage for your existing (unmodified) tests. It randomizes the thread schedules in a systematic and disciplined way, using an algorithm that provides probabilistic coverage guarantees.
- Dafny: a language and program verifier for functional correctnessDafny is an imperative object-based language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs.
- ChaliceChalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice.
- Boogie: An Intermediate Verification LanguageBoogie is an 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 verifiers for C and the verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes Boogie programs as input.
- VCC: A Verifier for Concurrent CVCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.
- Traver: Taming memory modelsTraver stands for Transformation Verification. The goal of the Traver project is to help programmers and compiler writers to understand the precise implications of program transformations of concurrent programs. Of particular interest are the effects of relaxed memory models, and how they impact the correctness of translations.
- HAVOCHAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation. The assertion logic of HAVOC allows the expression of properties of linked lists and arrays. The main challenge addressed by the tool are (1) tradeoff between expressiveness of the assertion logic and its computational efficiency, (2) generic inference techniques to relieve users of annotation burden for large modules.
- Code ContractsCode Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.
- Typed Assembly Language for Object-Oriented CompilersWe study techniques to guarantee safety properties of native code through typed intermediate languages and Typed Assembly Languages (TAL). TAL requires the compiler generate native code with type annotations and a verifier check the annotated native code. This way, we do not have to trust the compiler. We focus on large-scale optimizing object-oriented compilers.
- CHESS: Find and Reproduce Heisenbugs in Concurrent ProgramsCHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved debugging. CHESS is available for both managed and native programs.
- Pex and Moles - Isolation and White box Unit Testing for .NETPex automatically generates test suites with high code coverage using automated white box analysis. Pex is a Visual Studio add-in for testing .NET Framework applications. Moles supports unit testing by providing isolation by way of detours and stubs. The Moles framework is provided with Pex, or can be installed by itself as a Microsoft Visual Studio add-in.
- Spec#Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them.
- Sam Blackshear and Shuvendu Lahiri, Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings, in Programming Language Design and Implementation (PLDI'13), ACM, June 2013
- Manuel Fahndrich and Francesco Logozzo, Proceedings of the 20th Static Analysis Symposium, Springer Verlag, June 2013
- Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebelo, Towards Modularly Comparing Programs using Automated Theorem Provers, in International Conference on Automated Deduction (CADE '13), Springer, June 2013
- Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, no. MSR-TR-2013-34, March 2013
- Kenneth McMillan and Andrey Rybalchenko, Computing Relational Fixed Points using Interpolation, no. MSR-TR-2013-6, 17 January 2013
- Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo, Automatic Inference of Necessary Preconditions, in in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), Springer Verlag, January 2013
- Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett, An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Francesco Logozzo and Tom Ball, Modular and Verified Automatic Program Repair, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett, A Semantic Integrated Development Environment, in Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), ACM SIGPLAN, October 2012
- Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Rebelo, SymDiff: A language-agnostic semantic diff tool for imperative programs, in Computer Aided Verification (CAV '12) (Tool description), Springer, July 2012