ABSTRACT. UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. In this talk we will present new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.

ABSTRACT. Boolean satisfiability is a fundamental problem in computer science with a wide range of applications including planning, configuration management, design and verification of software/hardware systems. The annual SAT competition continues to witness impressive improvements in the performance of the winning SAT solvers largely thanks to the development of new heuristics arising out of intensive collaborative research in the SAT community. Modern SAT solvers achieve scalability and robustness with complex heuristics that are challenging to understand and explain. Consequently, the development of new algorithmic insights has been largely restricted to experts in the SAT community.

I will describe our project that boldly aims to democratise the design of SAT solvers. In particular, our project, called CrystalBall, seeks to develop a framework to provide white-box access to the execution of SAT solver that can aid both SAT solver developers and users to synthesize algorithmic heuristics for modern SAT solvers?We view modern conflict-driven clause learning (CDCL) solvers as a composition of classifiers and regressors for different tasks such as branching, clause memory management, and restarting, and we aim to provide a data-driven automated heuristic design mechanism that can allow experts in domains outside SAT community to contribute to the development of SAT solvers.

ABSTRACT. This talk will give a hands-on introduction to the software verification infrastructure consisting of the Horn solver Eldarica and the C model checker TriCera. After giving a high-level overview, the presenter will provide examples on how the tools can be used / extended for prototyping research ideas. Both tools are open-source and implemented in Scala.

Eldarica is a Horn solver that supports, among others, Horn clauses over the theories of integers, algebraic data-types, bit-vectors, arrays and the novel theory of heaps that simplifies encoding programs with heaps. Input clauses go through several preprocessing stages such as slicing, reachability analysis and inlining before being passed on to the main CEGAR engine that attempts to construct an abstract reachability graph that witnesses their satisfiability.

TriCera is a model checker for C programs that encodes input programs and specifications into a set of Horn clauses that can then be input to a Horn solver such as Eldarica or Z3/Spacer. TriCera mainly uses Eldarica for this purpose due to the tight integration of the tools and the theory of heaps. TriCera accepts most programs written in C11, and provides several other features useful for researchers: - the declaration and usage of uninterpreted predicates that can be seen as a form of inline assembler for Horn clauses, which simplify experimenting with various encodings, - automatic inference of loop invariants and function contracts, - parsing ACSL function contracts, - timing constraints in C programs (similar to UPPAAL timed automata), - concurrency.

ABSTRACT. I will report on a number of tools we have designed and implemented for the analysis of multi-threaded C programs. Our solutions share the common pattern of rewriting the original program into an equivalent non-deterministic sequential C program that is then fed to an existing well-performing model-checking tool for the analysis. Our translations have been optimized to take maximum advantage of the back-end technology used for the analysis. Using this paradigm we have designed a few bug-finding approaches that use back-ends based on bounded model-checking, as well as approaches to prove the correctness of programs. I will also report on recent approaches that we are developing to develop distributed bug-finding algorithms that make use of the large availability of processors provided by computer clusters or cloud computing platforms.

ABSTRACT. Constrained Horn Clauses (CHCs) is a fragment of First Order Logic (FOL), that has gained a lot of attention in recent years. One of the main reasons for the rising interest in CHCs is the ability to reduce many verification problems to satisfiability of CHCs. For example, program verification can naturally be described as the satisfiability of CHCs modulo a background theory such as linear arithmetic and arrays. To this end, CHC-solvers can be used as the back-end for different verification tools and allow to separate the generation of verification conditions from the decision procedure that decides if the verification conditions are correct or not.

In this talk, we present a novel framework, called LazyHorn, that is aimed at solving the satisfiability problem of CHCs modulo a background theory. The framework is driven by the idea that a set of CHCs can be solved in parts, making it an easier problem for the CHC-solver. Furthermore, solving a set of CHCs can benefit from an interpretation revealed by the solver for its subsets. LazyHorn is lazy in that it gradually extends the set of checked CHCs, as needed. It is also incremental in its use of a CHC solver, supplying it with an interpretation, obtained for previously checked subsets. We have implemented an efficient instance of the framework that is restricted to a fragment of CHCs called linear CHCs.

ABSTRACT. Program synthesis is the problem of generating a program to satisfy a specification of user intent. Since these specifications are usually partial, this means searching a space of candidate programs for one that exhibits the desired behavior. A lion’s share of the work on program synthesis focuses on new ways to perform the search, but allowing the user to communicate intent remains a major challenge.

This talk focuses on the complex relationship between user intent, specifications, and interaction model. In the domain of program synthesis, we narrow our focus by targeting a more specific category of users. Focusing on any subgroup of users allows making assumptions on both the input the user can generate for the synthesizer and the output they can consume. In the case of developers, concepts that are part of the programmer’s life such as code review and read-eval-print loops (REPL) can be leveraged for interactions with a synthesizer. The talk describes two synthesis-based tools that both leverage and cater to programmers as their users.

These assumptions also drive ways in which the hard problems of formal methods can be delegated to incomplete assistants: (bounded resource) solvers are a community favorite, and ML models are also gaining traction as an approach for deciding a hard subproblem. A third option, less sound than a solver and less decisive than a model, is a human: delegating parts of the task back to the user ensures that they are solved to the user's satisfaction. But how to make the user work for the tool, rather than the other way around, is a critical issue that must be addressed at the intersection of intent, specification, and interaction model.

Synthesizer design shows us how these elements can be at odds with each other, in particular the tension between the interface and state of the art synthesis techniques. Synthesis is, at best, a computationally hard problem, and many existing program synthesis tools and techniques were designed around the synthesizer and its internals, their user interface dictated by the needs of the synthesizer. We demonstrate the process of concurrently building both the synthesizer and its intended user-facing tool as a way to search for a balance of the needs of the interaction model (and, implicitly, the user) and the algorithm.

ABSTRACT. Ethereum Smart Contracts become a widely adopted technology to buildDecentralized Financial Applications (DeFis) and as such, they alreadyhold 200 billion USDs. Consequently, bugs in smart contracts can beexploited by malicious users and can lead to losses at the scale ofmillions or even billions of USDs. To prevent such situations fromhappening, there has been a growing interest in developing scalableformal verification techniques for this domain. In this talk, we willspecifically focus on the architecture of the Certora VerificationTool, i.e. an industrial standard automated prover technology toverify smart contracts. Besides a brief overview of the overall toolarchitecture, we will focus mainly on the SMT-based subroutines,including features such as domain-specific CEGAR methodology,distributed solver-portfolio approach, or techniques to share andexploit information between individual SMT solvers.

ABSTRACT. Amazon Web Services (AWS) authorizes over 43 trillion requests per day [1]. AWS has a custom language for specifying access control policies and a corresponding authorization engine. For each request, the authorization engine determines whether access should be granted or denied based on the relevant policies. In this talk, we describe our experience verifying the authorization engine in the context of a large, actively developed code base where many developers are not familiar with formal methods. We use Dafny, a verification-aware programming language, to specify authorization at a high level, implement it efficiently, and prove properties of the algorithm.

Authorization executes on a JVM, so we decided to compile the Dafny implementation to Java. To earn trust with developers, we insisted at the start that any generated code should be reviewable by anyone familiar with Java.  Dafny's built-in Java compiler does not generate readable code, so we wrote a custom compiler that generates idiomatic Java from our Dafny implementation. The Java code is reviewed in the same way as every other piece of code at Amazon.

Beyond human code review of the generated code, we use a multi-layered approach to ensure the correctness of the custom compiler: We verify compiler passes in Dafny, but also use techniques such as standard software testing and fuzzing.  Additionally, our compiler generates program annotations which let us leverage the capabilities of well-established software analysis tools such as CheckerFramework, to establish properties of the generated code such as null-correctness.

[1] https://aws.amazon.com/blogs/aws/happy-10th-birthday-aws-identity-and-access-management/