RISE Working Group on Formal Methods

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.

 

Projects
  • Automata
    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
    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.
  • bex
    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
    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.
  • Jennisys
    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.
Publications