ABSTRACT. Register automata are an expressive model of computation using finite memory. Conformance checking of their properties can be reduced to NonEmptiness tests, however, this problem is PSPACE-complete. Existing approaches usually employ symbolic state exploration, however, this results in state explosion for most complex register automata. We propose a semantics-preserving transformation of register automata into a representation in which reachability of states is equivalent to reachability of locations, i.e., is in NL. We evaluate the algorithm on random-generated and real-world automata and show that it avoids state explosion and performs efficiently. This yields a practical approach to conformance checking of register automata.

ABSTRACT. Binary Decision Diagrams (BDDs) are compact data structures used to efficiently store and process boolean functions. BDDs have many uses, from system design to model checking to efficiently storing context information for context-sensitive analysis. The use of BDDs in verification and program analysis has been facilitated by the recent emergence of many open source BDD libraries. The correctness of BDD-based system design and verification hinges upon the correctness of the BDD library implementations, and the correct use of these libraries. Surprisingly, for a technology so prevalent in system design and formal verification, there has been little research effort on formally verifying the correctness of BDD library implementations or their use. For BDD libraries that do perform some correctness checks, these are mostly confined to runtime assertion checking, which slows down BDD operations and might still be unable to reveal errors until deployment. To address these issues and take a step toward provably correct, yet efficient, BDD-handling code, we propose a formal system called BDDL to describe, reason about, and prove the correctness of BDD operations. BDDL extends lambda calculus with support for BDD operations (e.g., creation, manipulation), expressing BDD structural properties (e.g., canonicity, proper ordering), and BDD semantics (e.g., sets, relations). BDDL uses a type system based on refinement types to statically check BDD manipulation. We have proved our system correct using a small-step semantics and standard notions of progress and preservation. BDDL is the first attempt to provide a well-defined syntax and semantics to BDD operations; we show how it could prevent bugs and semantic errors in the implementation and use of three mature DD libraries.

ABSTRACT. Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users’ knowledge on how to apply the induction tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induction tactic, the SeLFiE interpreter judges whether the arguments are plausible for that problem according to the heuristic by examining both the syntactic structure of the problem and definitions of the relevant constants. To examine the intricate interaction between syntactic analysis and analysis of constant definitions, we introduce definitional quantifiers. For evaluation we build an automatic induction prover using SeLFiE. Our evaluation based on 347 inductive problems shows that our new prover achieves 1.4 x 10^3% improvement over the corresponding baseline prover for 1.0 second of timeout and the median value of speedup is 4.48x.

ABSTRACT. Ensuring correctness of verification tools is equally important as the correctness of the actual problems they try to establish. In this paper we evaluate automated fuzzing and debugging techniques applied to state-of-the-art multiplier verification tools, which take the common gate-level representation of and-inverter graphs as input. With a generation and mutation based fuzzing approach our tools are able to uncover major faults in verification tools including crashes as well as inaccurate verification results. We further apply delta debugging techniques and show their effectiveness in reducing failure-inducing inputs.

ABSTRACT. Symbolic execution has been a popular method for detecting vulnerabilities of programs in recent years, yet path explosion has remained a significant challenge in its application. This paper proposes a method for improving the efficiency of symbolic execution and detecting heap overflow vulnerability in executable codes. Instead of applying symbolic execution to the whole program, our method initially determines test units of the program, which are parts of the code that might contain heap overflow vulnerability. This is performed through static analysis and based on the specification of heap overflow vulnerability. Then, it applies symbolic execution to the test units and extracts a constraint tree for each unit. Every node in this tree contains the path and vulnerability constraints on the unit input data for executing and overflowing heap buffers in that node. Solving these constraints gives us input values for the test unit that execute the desired nodes and cause heap overflow. Finally, we use curve fitting and treatment learning to approximate the relation between system and unit input data as a function. Using this function, we generate system inputs that enter the program, reach vulnerable instructions in the desired test unit, and cause heap overflow in those instructions. This method is implemented as a plugin for angr framework and evaluated using a group of benchmark programs. The experiments show its superiority over similar tools in accuracy and performance.

ABSTRACT. A common problem in verification is to ensure that the formal specification models the real-world system, i.e., the implementation, faithfully. Testing is a technique that can help to bridge the gap between a formal specification and its implementation.

Fuzzing in general and grammar-based fuzzing in particular are successfully used for finding bugs in implementations. Traditional fuzzing applications rely on an implicit test specification that informally can be described as ``the program under test does not crash''.

In this paper, we present an approach using grammar-based fuzzing to ensure the conformance of a formal specification to a real-world implementation. For this, we derive an executable test-oracle from a formal specification expressed in Isabelle/HOL that is used during the fuzzing of the implementation. We discuss our approach using a formal semantics of Solidity as case study.