Our Mission: The Formal Methods (FMx) working group explores the mathematical (including logical and statistical) foundations of software systems. We develop theories and techniques for rigorously specifying and synthesizing software systems, and computer-aided methods for reasoning about them.
Automata is a .NET tool kit that provides facilities for manipulating and analyzing regular expressions, symbolic finite automata, and symbolic finite transducers. It supports automata and transducers where input and output alphabets can be fully symbolic. Constraints over the alphabets can be analyzed using Satisfiability Modulo Theory (SMT) solvers. The tool kit provides a particular extension that uses the Microsoft SMT solver Z3.
BEK is a domain specific language for writing common string functions, combined with state of the art analysis. With BEK, you can answer questions like Do these two programs output the same string? Can this program ever output a target string? What happens if I compose these two programs? Does the order matter? More general than regular expressions, BEK has been specifically tailored to capture common idioms in string manipulating functions.
A domain specific language for writing and analyzing string encoders and decoders.
- DKAL: Distributed Knowledge Authorization Language
DKAL is a high-level policy language, especially for federated scenarios. It was originally created with authorization policies in mind but it is not limited to authorization policies and can be applied to any other policies. As a part of the DKAL project we developed information logic (logic of infons). DKAL’s world is distributed. Principals compute their knowledge and exchange information.
Duality 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.
- FORMULA - Modeling Foundations
FORMULA specifications are highly declarative logic programs that can express rich synthesis and verification problems. FORMULA 2.0 is optimized for formally specifying domain-specific languages (DSLs) and model transformations. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA supports synthesis, verification, and design space exploration.
- Interpolating Z3
Interpolating Z3 uses Z3's proof generation capability to generate Craig interpolants in the first-order theory of uninterpreted functions, arrays and linear arithmetic.
This is where programs begin. Jennisys is a programming language that emphasizes clean public interfaces and lets programmers describe the data structures they intend a private implementation to use. Code is underemphasized, and Jennisys attempts to synthesize code automatically from the public interface and the given data-structure description.
- Rex - Regular Expression Exploration
Rex is a tool that explores .NET regexes and generates members efficiently.
- Z3: Theorem Prover
Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research.
- Kenneth McMillan and Andrey Rybalchenko, Computing Relational Fixed Points using Interpolation, no. MSR-TR-2013-6, 17 January 2013
- Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi, What's Decidable About Weak Memory Models?, in 21st European Symposium on Programming (ESOP 2012), Springer, 26 March 2012
- Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang, Concurrent Library Correctness on the TSO Memory Model, in 21st European Symposium on Programming (ESOP 2012), Springer, 26 March 2012
- K. Rustan M. Leino and Aleksandar Milicevic, Program Extrapolation with Jennisys, no. MSR-TR-2012-12, February 2012
- Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjorner, Symbolic Finite State Transducers: Algorithms and Applications, in POPL’12, ACM SIGPLAN, January 2012
- Margus Veanes and Nikolaj Bjorner, Alternating simulation and IOCO, in International Journal on Software Tools for Technology Transfer (STTT) , Springer, November 2011
- Kenneth L. McMillan, Interpolants from Z3 proofs, in Formal Methods in Computer-Aided Design, 30 October 2011
- Ethan Jackson, Tihamer Levendovszky, and Daniel Balasubramanian, Reasoning about Metamodeling with Formal Specifications and Automatic Proofs, in MODELS 2011, 2011
- Ethan Jackson, Nikolaj Bjorner, and Wolfram Schulte, Canonical Regular Types, in ICLP, 2011
- Sergey Pupyrev, Lev Nachmanson, Sergey Bereg, and Alexander E. Holroyd, Edge Routing with Ordered Bundles, in Graph Drawing, 2011
- Md. Ashfaquzzaman Khan, Richard Neil Pittman, and Alessandro Forin, gNOSIS: A Board-level Debugging and Verification Tool, no. MSR-TR-2010-106, 30 July 2010
- Sergey Pupyrev, Lev Nachmanson, and Michael Kaufmann, Improving Layered Graph Layouts with EdgeBundling, in Graph Drawing, 2010
- Ethan K. Jackson, Eunsuk Kang, Markus Dahlweid, Dirk Seifert, and Thomas Santen, Components, platforms and possibilities: towards generic automation for MDA, in EMSOFT, ACM, 2010
- Weiqin Ma, Jyh-Charn Liu, and Alessandro Forin, Design and Testing of a CPU Emulator, no. MSR-TR-2009-115, 21 August 2009