Leveraging Control Flow Knowledge in SMT Solving of Program Verification

2021 ◽  
Vol 30 (4) ◽  
pp. 1-26
Author(s):  
Jianhui Chen ◽  
Fei He
Keyword(s):  
Program Verification ◽  
Search Space ◽  
General Purpose ◽  
Control Flow ◽  
Satisfiability Modulo Theories ◽  
Useful Knowledge ◽  
Smt Solver ◽  
Software Analysis ◽  
Smt Solving ◽  
Novel Approach

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, current SMT solvers are designed for the general purpose of constraint solving. Lots of useful knowledge of programs cannot be utilized during SMT solving. As a result, the SMT solver may spend much effort to explore redundant search space. In this article, we propose a novel approach to utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced, and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks. The results show significant improvements of our approach.

scholarly journals Syntax-Guided Quantifier Instantiation

2021 ◽  
pp. 145-163
Author(s):  
Aina Niemetz ◽  
Mathias Preiner ◽  
Andrew Reynolds ◽  
Clark Barrett ◽  
Cesare Tinelli
Keyword(s):  
State Of The Art ◽  
Satisfiability Modulo Theories ◽  
Floating Point ◽  
New Approach ◽  
Smt Solver ◽  
Floating Point Arithmetic ◽  
Novel Approach ◽  
Non Linear ◽  
Quantifier Instantiation ◽  
Point Arithmetic

AbstractThis paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.

Applications and Challenges in Satisfiability Modulo Theories

10.29007/cl74 ◽  
2018 ◽  
Author(s):  
Leonardo De Moura ◽  
Nikolaj Bjorner
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problem ◽  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
Invariant Generation ◽  
Software Analysis ◽  
The Core ◽  
Precise Analysis ◽  
System States ◽  
Automatic Theorem

The area of software analysis, testing and verification is now undergoing a revolution thanks to the use of automated and scalable support for logical methods. A well-recognized premise is that at the core of software analysis engines is invariably a component using logical formulas for describing states and transformations between system states. One can thus say that symbolic logic is the calculus of computation. The process of using this information for discovering and checking program properties (including such important properties as safety and security) amounts to automatic theorem proving. In particular, theorem provers that directly support common software constructs offer a compelling basis. Such provers are commonly called satisfiability modulo theories (SMT) solvers.Z3 is the leading SMT solver. It is developed by the authors at Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories such as arithmetic, bit-vectors, lists, records and arrays.This paper examines three applications of Z3 in the context of invariant generation.The first lets Z3 infer invariants as a constraint satisfaction problem, the second applicationillustrates the use of Z3 for bit-precise analysis and our third application exemplifiesusing Z3 for calculations.

scholarly journals FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

2021 ◽  
pp. 152-169
Author(s):  
Margarida Ferreira ◽  
Miguel Terra-Neves ◽  
Miguel Ventura ◽  
Inês Lynce ◽  
Ruben Martins
Keyword(s):  
Real World ◽  
Regular Expression ◽  
User Interaction ◽  
Search Space ◽  
Satisfiability Modulo Theories ◽  
Experimental Results ◽  
Divide And Conquer ◽  
Regular Expressions ◽  
Smt Solver ◽  
Synthesis Procedure

AbstractForm validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users.We present Forest, a regular expression synthesizer for digital form validations. Forest produces a regular expression that matches the desired pattern for the input values and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesize capture conditions for a given regular expression. To increase confidence in the synthesized regular expression, we implement user interaction based on distinguishing inputs.We evaluated Forest on real-world form-validation instances using regular expressions. Experimental results show that Forest successfully returns the desired regular expression in 70% of the instances and outperforms Regel, a state-of-the-art regular expression synthesizer.

scholarly journals Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories

2011 ◽  
Vol 40 ◽  
pp. 701-728 ◽  
Author(s):  
A. Cimatti ◽  
A. Griggio ◽  
R. Sebastiani
Keyword(s):  
Empirical Test ◽  
Main Idea ◽  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
The Core ◽  
Reduction Techniques ◽  
Novel Approach ◽  
Suitable Amount ◽  
Core Reduction ◽  
Unsatisfiable Core

The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT. Surprisingly, the problem of finding unsatisfiable cores in SMT has received very little attention in the literature. In this paper we present a novel approach to this problem, called the Lemma-Lifting approach. The main idea is to combine an SMT solver with an external propositional core extractor. The SMT solver produces the theory lemmas found during the search, dynamically lifting the suitable amount of theory information to the Boolean level. The core extractor is then called on the Boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas are removed. The approach is conceptually interesting, and has several advantages in practice. In fact, it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play manner, so as to benefit for free of all unsat-core reduction techniques which have been or will be made available. We have evaluated our algorithm with a very extensive empirical test on SMT-LIB benchmarks, which confirms the validity and potential of this approach.

scholarly journals Lookahead-Based SMT Solving

10.29007/gzzf ◽  
2018 ◽  
Author(s):  
Antti Hyvärinen ◽  
Matteo Marescotti ◽  
Parvin Sadigova ◽  
Hana Chockler ◽  
Natasha Sharygina
Keyword(s):  
Upper Bound ◽  
Binary Tree ◽  
Search Space ◽  
Divide And Conquer ◽  
Constraint Solving ◽  
Prototype Implementation ◽  
Smt Solver ◽  
Smt Solving ◽  
Clause Learning

The lookahead approach for binary-tree-based search in constraint solving favors branching that provide the lowest upper bound for the remaining search space. The approach has recently been applied in instance partitioning in divide-and-conquer-based parallelization, but in general its connection to modern, clause-learning solvers is poorly understood. We show two ways of combining lookahead approach with a modern DPLL(T)-based SMT solver fully profiting from theory propagation, clause learning, and restarts. Our thoroughly tested prototype implementation is surprisingly efficient as an independent SMT solver on certain instances, in particular when applied to a non-convex theory, where the lookahead-based implementation solves 40% more unsatisfiable instances compared to the standard implementation.

Engineering Theories with Z3

10.29007/x7b4 ◽  
2018 ◽  
Author(s):  
Nikolaj Bjorner
Keyword(s):  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
Testing Tools ◽  
Software And Hardware ◽  
Design And Testing

Modern Satisfiability Modulo Theories (SMT)solvers are fundamental to many programanalysis, verification, design and testing tools. They are a goodfit for the domain of software and hardware engineering becausethey support many domains that are commonly used by the tools.The meaning of domains are captured by theories that can beaxiomatized or supported by efficient <i>theory solvers</i>.Nevertheless, not all domains are handled by all solvers andmany domains and theories will never be native to any solver.We here explore different theories that extend MicrosoftResearch's SMT solver Z3's basicsupport. Some can be directly encoded or axiomatized,others make use of user theory plug-ins.Plug-ins are a powerful way for tools to supply their custom domains.

Implementing and using finite automata toolkits

1996 ◽  
Vol 2 (4) ◽  
pp. 295-302 ◽  
Author(s):  
BRUCE W. WATSON
Keyword(s):  
Flight Control ◽  
Program Verification ◽  
Finite Automata ◽  
Circuit Simulation ◽  
Implementation Strategies ◽  
Digital Circuit ◽  
General Purpose ◽  
Genetic Sequencing ◽  
Java Program ◽  
Fire Engine

Finite automata and various extensions of them, such as transducers, are used in areas as diverse as compilers, spelling checking, natural language grammar checking, communication protocol design, digital circuit simulation, digital flight control, speech recognition and synthesis, genetic sequencing, and Java program verification. Unfortunately, as the number of applications has grown, so has the variety of implementations and implementation techniques. Typically, programmers will be confused enough to resort to their text books for the most elementary algorithms. Recently, advances have been made in taxonomizing algorithms for constructing and minimizing automata and in evaluating various implementation strategies Watson 1995. Armed with this, a number of general-purpose toolkits have been developed at universities and companies. One of these, FIRE Lite, was developed at the Eindhoven University of Technology, while its commercial successor, FIRE Engine II, has been developed at Ribbit Software Systems Inc. Both of these toolkits provide implementations of all of the known algorithms for constructing automata from regular expressions, and all of the known algorithms for minimizing deterministic finite automata. While the two toolkits have a great deal in common, we will concentrate on the structure and use of the noncommercial FIRE Lite. The prototype version of FIRE Lite was designed with compilers in mind. More recently, computation linguists and communications protocol designers have become interested in using the toolkit. This has led to the development of a much more general interface to FIRE Lite, including the support of both Mealy and Moore regular transducers. While such a toolkit may appear extremely complex, there are only a few choices to be made. We also consider a ‘recipe’ for making good use of the toolkits. Lastly, we consider the future of FIRE Lite. While FIRE Engine II has obvious commercial value, we are committed to maintaining a version which is freely available for academic use.

scholarly journals SMT-Based Contention-Free Task Mapping and Scheduling on 2D/3D SMART NoC with Mixed Dimension-Order Routing

2022 ◽  
Vol 19 (1) ◽  
pp. 1-21
Author(s):  
Daeyeal Lee ◽  
Bill Lin ◽  
Chung-Kuan Cheng
Keyword(s):  
System Performance ◽  
Search Space ◽  
Satisfiability Modulo Theories ◽  
Low Latency ◽  
Task Mapping ◽  
Single Cycle ◽  
Space Reduction ◽  
Reduction Techniques ◽  
2D And 3D ◽  
Mixed Dimension

SMART NoCs achieve ultra-low latency by enabling single-cycle multiple-hop transmission via bypass channels. However, contention along bypass channels can seriously degrade the performance of SMART NoCs by breaking the bypass paths. Therefore, contention-free task mapping and scheduling are essential for optimal system performance. In this article, we propose an SMT (Satisfiability Modulo Theories)-based framework to find optimal contention-free task mappings with minimum application schedule lengths on 2D/3D SMART NoCs with mixed dimension-order routing. On top of SMT’s fast reasoning capability for conditional constraints, we develop efficient search-space reduction techniques to achieve practical scalability. Experiments demonstrate that our SMT framework achieves 10× higher scalability than ILP (Integer Linear Programming) with 931.1× (ranges from 2.2× to 1532.1×) and 1237.1× (ranges from 4× to 4373.8×) faster average runtimes for finding optimum solutions on 2D and 3D SMART NoCs and our 2D and 3D extensions of the SMT framework with mixed dimension-order routing also maintain the improved scalability with the extended and diversified routing paths, resulting in reduced application schedule lengths throughout various application benchmarks.

scholarly journals Scheduling Optimization of Time-Triggered Cyber-Physical Systems Based on Fuzzy-Controlled QPSO and SMT Solver

Energies ◽  
2020 ◽  
Vol 13 (3) ◽  
pp. 668
Author(s):  
Jie Jian ◽  
Lide Wang ◽  
Huang Chen ◽  
Xiaobo Nie
Keyword(s):  
Scheduling Algorithm ◽  
Cyber Physical Systems ◽  
Satisfiability Modulo Theories ◽  
Random Mutation ◽  
Physical Systems ◽  
Smt Solver ◽  
Time Requirements ◽  
Adaptive Adjustment ◽  
Periodic Traffic ◽  
Cost Efficient

The time-triggered communication paradigm is a cost-efficient way to meet the real-time requirements of cyber-physical systems. It is a non-deterministic polynomial NP-complete problem for multi-hop networks and non-strictly periodic traffic. A two-level scheduling approach is proposed to simplify the complexity during optimization. In the first level, a fuzzy-controlled quantum-behaved particle swarm optimization (FQPSO) algorithm is proposed to optimize the scheduling performance by assigning time-triggered frame instances to the basic periods of each link. In order to prevent population from high aggregation, a random mutation mechanism is used to disturb particles at the aggregation point and enhance the diversity at later stages. Fuzzy logic is introduced and well designed to realize a dynamic adaptive adjustment of the contraction–expansion coefficient and mutation rate in FQPSO. In the second level, we use an improved Satisfiability Modulo Theories (SMT) scheduling algorithm to solve the collision-free and temporal constraints. A schedulability ranking method is proposed to accelerate the computation of the SMT-based incremental scheduler. Our approach can co-optimize the jitter and load balance of communication for an off-line schedule. The experiments show that the proposed approach can improve the performance of the scheduling table, reduce the optimization time, and reserve space for incremental messages.

Sign in / Sign up

Export Citation Format

Share Document