A Unified Framework for DPLL(T) + Certificates

Satisfiability Modulo Theories (SMT) techniques are widely used nowadays. SMT solvers are typically used as verification backends. When an SMT solver is invoked, it is quite important to ensure the correctness of its results. To address this problem, we propose a unified certificate framework based on DPLL(T), including a uniform certificate format, a unified certificate generation procedure, and a unified certificate checking procedure. The certificate format is shown to be simple, clean, and extensible to different background theories. The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. The soundness and completeness for DPLL(T) + certificates were established. The certificate checking procedure is straightforward and efficient. Experimental results show that the overhead for certificates generation is only 10%, which outperforms other methods, and the certificate checking procedure is quite time saving.

Download Full-text

Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT

Proceedings of the Institute for System Programming of RAS ◽

10.15514/ispras-2021-33(4)-13 ◽

2021 ◽

Vol 33 (4) ◽

pp. 177-194

Author(s):

Rafael Faritovich Sadykov ◽

Mikhail Usamovich Mandrykin

Keyword(s):

Program Verification ◽

Source Code ◽

Decision Procedures ◽

C Programs ◽

Smt Solver ◽

Smt Solvers ◽

Relevant Logics ◽

Soundness And Completeness ◽

C Program ◽

Quantifier Instantiation

The process of developing C programs is quite often prone to errors related to the uses of pointer arithmetic and operations on memory addresses. This promotes a need in developing various tools for automated program verification. One of the techniques frequently employed by those tools is invocation of appropriate decision procedures implemented within existing SMT-solvers. But at the same time both the SMT standard and most existing SMT-solvers lack the relevant logics (combinations of logical theories) for directly and precisely modelling the semantics of pointer operations in C. One of the possible ways to support these logics is to implement them in an SMT solver, but this approach can be time-consuming (as requires modifying the solver’s source code), inflexible (introducing any changes to the theory’s signature or semantics can be unreasonably hard) and limited (every solver has to be supported separately). Another way is to design and implement custom quantifier instantiation strategies. These strategies can be then used to translate formulas in the desired theory combinations to formulas in well-supported decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper presents an informal description of this proof of the proposed procedure. The theory of bounded pointer arithmetic itself was formulated based on known errors regarding the correct use of pointer arithmetic operations in industrial code as well as the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.

Download Full-text

AVATAR Modulo Theories

10.29007/k6tp ◽

2018 ◽

Author(s):

Giles Reger ◽

Nikolaj Bjorner ◽

Martin Suda ◽

Andrei Voronkov

Keyword(s):

Theorem Proving ◽

Satisfiability Modulo Theories ◽

Theorem Prover ◽

Ground Theory ◽

Smt Solver ◽

First Order ◽

Proof Search ◽

Smt Solvers ◽

Sat Solver ◽

A New Technique

This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.

Download Full-text

FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-72016-2_9 ◽

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.

Download Full-text

νZ - Maximal Satisfaction with Z3

10.29007/jmxj ◽

2018 ◽

Author(s):

Nikolaj Bjorner ◽

Anh-Dung Phan

Keyword(s):

Theorem Proving ◽

Optimization Problems ◽

Linear Optimization ◽

Satisfiability Modulo Theories ◽

Objective Functions ◽

Smt Solver ◽

Smt Solvers ◽

Free Variables ◽

Linear Optimization Problems ◽

Pareto Fronts

Satisfiability Modulo Theories, SMT, solvers are used inmany applications. These applications benefit from thepower of tuned and scalable theorem proving technologiesfor supported logics and specialized theory solvers.SMT solvers are primarily used to determine whether formulas are satisfiable.Furthermore, when formulas are satisfiable, many applications need modelsthat assign values to free variables.Yet, in many cases arbitrary assignments are insufficient,and what is really needed is an <i>optimal</i> assignmentwith respect to objective functions. So far, users of Z3,an SMT solver from Microsoft Research, build custom loopsto achieve objective values. This is no longer necessarywith νZ (new-Z, or max-Z), an extension within Z3 that letsusers formulate objective functions directly with Z3. Under the hood there is aportfolio of approaches for solving linear optimization problems overSMT formulas, MaxSMT, and their combinations. Objective functions are combinedas either Pareto fronts, lexicographically, or each objective is optimized independently.

Download Full-text

A Platform for Placement of Analog Integrated Circuits Using Satisfiability Modulo Theories

Journal of Circuits System and Computers ◽

10.1142/s021812661650047x ◽

2016 ◽

Vol 25 (05) ◽

pp. 1650047

Author(s):

Sherif M. Saif ◽

Mohamed Dessouky ◽

M. Watheq El-Kharashi ◽

Hazem Abbas ◽

Salwa Nassar

Keyword(s):

Integrated Circuits ◽

Design Automation ◽

Electronic Design Automation ◽

Analog Integrated Circuits ◽

Satisfiability Modulo Theories ◽

Physical Constraints ◽

Smt Solver ◽

Smt Solvers ◽

Feasible Solutions ◽

The Given

Satisfiability modulo theories (SMT) is an area concerned with checking the satisfiability of logical formulas over one or more theories. SMT can be well tuned to solve several of the most intriguing problems in electronic design automation (EDA). Analog placers use physical constraints to automatically generate small sections of layout. The work presented in this paper shows that SMT solvers can be used for the automation of analog placement, given some physical constraints. We propose a tool that uses Microsoft Z3 SMT solver to find valid placement solutions for the given analog blocks. Accordingly, it generates multiple layouts that fulfill some given constraints and provides a variety of alternative layouts. The user has the option to choose one of the feasible solutions. The proposed system uses the quantifier-free linear real arithmetic (QFLRA), which makes the problem decidable. The proposed system is able to generate valid placement solutions for benchmarks. For benchmarks that have many constraints and few geometries, the proposed system achieves a speedup that is 10 times faster than other recently used approaches.

Download Full-text

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.

Download Full-text

Predicting the Success of Mediation Requests Using Case Properties and Textual Information for Reducing the Burden on the Court

Digital Government: Research and Practice (DGOV) ◽

10.1145/3469233 ◽

2021 ◽

Author(s):

Hsun-Ping Hsieh ◽

JiaWei Jiang ◽

Tzu-Hsin Yang ◽

Renfen Hu

Keyword(s):

Real World ◽

Experimental Results ◽

Criminal Cases ◽

Time Saving ◽

Textual Information ◽

Negotiation Skill ◽

Multiple Classifiers ◽

Legal Case ◽

Textual Data ◽

F Measure

The success of mediation is affected by many factors, such as the context of the quarrel, personality of both parties, and the negotiation skill of the mediator, which lead to uncertainty for the predicting work. This paper takes a different approach from previous legal prediction research. It analyzes and predicts whether two parties in a dispute can reach an agreement peacefully through the conciliation of mediation. With the inference result, we can know if the mediation is a more practical and time-saving method to solve the dispute. Existing works about legal case prediction mostly focus on prosecution or criminal cases. In this work, we propose a LSTM-based framework, called LSTMEnsembler, to predict mediation results by assembling multiple classifiers. Among these classifiers, some are powerful for modeling the numerical and categorical features of case information, e.g., XGBoost and LightGBM; and, some are effective for dealing with textual data, e.g., TextCNN and BERT. The proposed LSTMEnsembler aims to not only combine the effectiveness of different classifiers intelligently, but also capture temporal dependencies from previous cases to boost the performance of mediation prediction. Our experimental results show that our proposed LSTMEnsembler can achieve 85.6% for F-measure on real-world mediation data.

Download Full-text

Automatic Synthesis of Generalized Winning Strategies of Impartial Combinatorial Games Using SMT Solvers

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2020/236 ◽

2020 ◽

Author(s):

Kaisheng Wu ◽

Liangda Fang ◽

Liping Xiong ◽

Zhao-Rong Lai ◽

Yong Qiao ◽

...

Keyword(s):

Artificial Intelligence ◽

Game Theory ◽

Experimental Results ◽

Combinatorial Games ◽

Logical Framework ◽

Automatic Synthesis ◽

Integer Arithmetic ◽

Smt Solvers ◽

Winning Strategies

Strategy representation and reasoning has recently received much attention in artificial intelligence. Impartial combinatorial games (ICGs) are a type of elementary and fundamental games in game theory. One of the challenging problems of ICGs is to construct winning strategies, particularly, generalized winning strategies for possibly infinitely many instances of ICGs. In this paper, we investigate synthesizing generalized winning strategies for ICGs. To this end, we first propose a logical framework to formalize ICGs based on the linear integer arithmetic fragment of numeric part of PDDL. We then propose an approach to generating the winning formula that exactly captures the states in which the player can force to win. Furthermore, we compute winning strategies for ICGs based on the winning formula. Experimental results on several games demonstrate the effectiveness of our approach.

Download Full-text

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

Energies ◽

10.3390/en13030668 ◽

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.

Download Full-text

Representing hybrid automata by action language modulo theories

Theory and Practice of Logic Programming ◽

10.1017/s1471068417000412 ◽

2017 ◽

Vol 17 (5-6) ◽

pp. 924-941 ◽

Cited By ~ 1

Author(s):

JOOHYUNG LEE ◽

NIKHIL LONEY ◽

YUNSONG MENG

Keyword(s):

Differential Equations ◽

Ordinary Differential Equations ◽

Satisfiability Modulo Theories ◽

Prototype System ◽

Hybrid Automata ◽

Action Languages ◽

Smt Solver ◽

Action Language ◽

Linear Hybrid Automata ◽

Answer Set

AbstractBoth hybrid automata and action languages are formalisms for describing the evolution of dynamic systems. This paper establishes a formal relationship between them. We show how to succinctly represent hybrid automata in an action language which in turn is defined as a high-level notation for answer set programming modulo theories—an extension of answer set programs to the first-order level similar to the way satisfiability modulo theories (SMT) extends propositional satisfiability (SAT). We first show how to represent linear hybrid automata with convex invariants by an action language modulo theories. A further translation into SMT allows for computing them using SMT solvers that support arithmetic over reals. Next, we extend the representation to the general class of non-linear hybrid automata allowing even non-convex invariants. We represent them by an action language modulo ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present a prototype systemcplus2aspmtbased on these translations, which allows for a succinct representation of hybrid transition systems that can be computed effectively by the state-of-the-art SMT solverdReal.

Download Full-text