Search Results

SMT-based verification of low-level code requires modeling and reasoning about memory operations. Prior work has shown that optimizing memory representations is beneficial for scaling verification—pointer analysis, for example can be used to split memory ...

With its combination of Datalog, SMT solving, and functional programming, the language Formulog provides an appealing mix of features for implementing SMT-based static analyses (e.g., refinement type checking, symbolic execution) in a natural, ...

During the last few years, BDD-based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, ...

SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to be challenging. If quantifier ...

This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and ...

Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent 'on the stand' to subject their ...

We present a new algorithm for solving string constraints. The algorithm builds upon a recent method for solving word equations and regular constraints that interprets string variables as languages rather than strings and, consequently, mitigates the ...

Recurrent neural networks are increasingly employed in safety-critical applications, such as control in cyber-physical systems, and therefore their verification is crucial for guaranteeing reliability and correctness. We present a novel approach ...

The query containment problem is a fundamental computer science problem which was originally defined for relational queries. With the growing popularity of the sparql query language, it became relevant and important in this new context:...

• Implementation and evaluation of open source sparql query containment solver SpeCS

Widespread use of string solvers in the formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context. Designing practical algorithms for the (...

We introduce user-propagators as a new feature of the Z3 SMT solver. User-propagation allows users to write custom theory extensions for Z3, by implementing callbacks via the Z3 API. These callbacks are invoked by Z3 and eliminate eager processing ...

ProB provides a constraint solver for the B-method written in Prolog and can make use of different backends based on SAT and SMT solving. One such backend translates B and Event-B operators to SMT-LIB using the Z3 solver. This translation uses ...

Provably correct software is one of the key challenges of our software-driven society. Program synthesis—the task of constructing a program satisfying a given specification—is one strategy for achieving this. The result of this task is then a program that ...

This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies ...

Static worst-case timing analyses compute safe timing bounds of applications running in real-time systems. These bounds are necessary to evaluate the strict timing constraints of real-time systems. Moreover, the inherent complexity of such systems ...

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on ...

Automated techniques and tools for the construction and analysis of systems are inevitable to manage the complexity of the current systems. Such techniques and tools are the subject of interest of the International Conference on Tools and ...

Improving code quality without changing its functionality, e.g., by refactoring or optimization, is an everyday programming activity. Good programming practice requires that each such change should be followed by a check if the change really ...

Symbolic execution is an essential approach for automated test case generation. However, the approach is generally not scalable to large programs. One critical reason is that the constraint solving problems in symbolic execution are generally hard. ...

Sparse program analysis is fast as it propagates data flow facts via data dependence, skipping unnecessary control flows. However, when path-sensitively checking millions of lines of code, it is still prohibitively expensive because a huge number of ...