-
Invariant Checking for SMT-based Systems with Quantifiers
Authors:
Gianluca Redondi,
Alessandro Cimatti,
Alberto Griggio,
Kenneth McMillan
Abstract:
This paper addresses the problem of checking invariant properties for a large class of symbolic transition systems, defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort (finite, but unbounded) to an interpreted sort, such as the the integers under the theory of linear arithmetic. This formalism is very expressive and can be used for…
▽ More
This paper addresses the problem of checking invariant properties for a large class of symbolic transition systems, defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort (finite, but unbounded) to an interpreted sort, such as the the integers under the theory of linear arithmetic. This formalism is very expressive and can be used for modeling parameterized systems, array-manipulating programs, and more. We propose two algorithms for finding universal inductive invariants for such systems. The first algorithm combines an IC3-style loop with a form of implicit predicate abstraction to construct an invariant in an incremental manner. The second algorithm constructs an under-approximation of the original problem, and searches for a formula which is an inductive invariant for this case; then, the invariant is generalized to the original case, and checked with a portfolio of techniques. We have implemented the two algorithms and conducted an extensive experimental evaluation, considering various benchmarks and different tools from the literature. As far as we know, our method is the first capable of handling in a large class of systems in a uniform way. The experiment shows that both algorithms are competitive with the state of the art.
△ Less
Submitted 29 February, 2024;
originally announced February 2024.
-
A Case Study in Analytic Protocol Analysis in ACL2
Authors:
Max von Hippel,
Panagiotis Manolios,
Kenneth L. McMillan,
Cristina Nita-Rotaru,
Lenore Zuck
Abstract:
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms acro…
▽ More
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms across the Internet. One key component in our RTO computation analysis was proving in ACL2s that for all alpha in [0, 1), the limit as n approaches infinity of alpha raised to n is zero. Whereas the most obvious proof strategy involves the logarithm, whose codomain includes irrationals, by default ACL2 only supports rationals, which forced us to take a non-standard approach. In this paper, we explore different approaches to proving the above result in ACL2(r) and ACL2s, from the perspective of a relatively new user to each. We also contextualize the theorem by showing how it allowed us to prove important asymptotic properties of the RTO computation. Finally, we discuss tradeoffs between the various proof strategies and directions for future research.
△ Less
Submitted 15 November, 2023;
originally announced November 2023.
-
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
Authors:
Wenxi Wang,
Yang Hu,
Mohit Tiwari,
Sarfraz Khurshid,
Kenneth McMillan,
Risto Miikkulainen
Abstract:
Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or re…
▽ More
Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve up to 5.2% and 7.4% more problems on two recent SAT competition problem sets, SATCOMP-2022 and SATCOMP-2023, respectively. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.
△ Less
Submitted 8 May, 2024; v1 submitted 26 October, 2021;
originally announced October 2021.
-
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Authors:
Oded Padon,
Jochen Hoenicke,
Kenneth L. McMillan,
Andreas Podelski,
Mooly Sagiv,
Sharon Shoham
Abstract:
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophe…
▽ More
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.
△ Less
Submitted 2 June, 2021;
originally announced June 2021.
-
Evaluation of Sampling Methods for Robotic Sediment Sampling Systems
Authors:
Jun Han Bae,
Wonse Jo,
Jee Hwan Park,
Richard M. Voyles,
Sara K. McMillan,
Byung-Cheol Min
Abstract:
Analysis of sediments from rivers, lakes, reservoirs, wetlands and other constructed surface water impoundments is an important tool to characterize the function and health of these systems, but is generally carried out manually. This is costly and can be hazardous and difficult for humans due to inaccessibility, contamination, or availability of required equipment. Robotic sampling systems can ea…
▽ More
Analysis of sediments from rivers, lakes, reservoirs, wetlands and other constructed surface water impoundments is an important tool to characterize the function and health of these systems, but is generally carried out manually. This is costly and can be hazardous and difficult for humans due to inaccessibility, contamination, or availability of required equipment. Robotic sampling systems can ease these burdens, but little work has examined the efficiency of such sampling means and no prior work has investigated the quality of the resulting samples. This paper presents an experimental study that evaluates and optimizes sediment sampling patterns applied to a robot sediment sampling system that allows collection of minimally-disturbed sediment cores from natural and man-made water bodies for various sediment types. To meet this need, we developed and tested a robotic sampling platform in the laboratory to test functionality under a range of sediment types and operating conditions. Specifically, we focused on three patterns by which a cylindrical coring device was driven into the sediment (linear, helical, and zig-zag) for three sediment types (coarse sand, medium sand, and silt). The results show that the optimal sampling pattern varies depending on the type of sediment and can be optimized based on the sampling objective. We examined two sampling objectives: maximizing the mass of minimally disturbed sediment and minimizing the power per mass of sample. This study provides valuable data to aid in the selection of optimal sediment coring methods for various applications and builds a solid foundation for future field testing under a range of environmental conditions.
△ Less
Submitted 23 June, 2020;
originally announced June 2020.
-
Bayesian Interpolants as Explanations for Neural Inferences
Authors:
Kenneth L. McMillan
Abstract:
The notion of Craig interpolant, used as a form of explanation in automated reasoning, is adapted from logical inference to statistical inference and used to explain inferences made by neural networks. The method produces explanations that are at the same time concise, understandable and precise.
The notion of Craig interpolant, used as a form of explanation in automated reasoning, is adapted from logical inference to statistical inference and used to explain inferences made by neural networks. The method produces explanations that are at the same time concise, understandable and precise.
△ Less
Submitted 8 April, 2020;
originally announced April 2020.
-
Learning Abstractions for Program Synthesis
Authors:
Xinyu Wang,
Greg Anderson,
Isil Dillig,
K. L. McMillan
Abstract:
Many example-guided program synthesis techniques use abstractions to prune the search space. While abstraction-based synthesis has proven to be very powerful, a domain expert needs to provide a suitable abstract domain, together with the abstract transformers of each DSL construct. However, coming up with useful abstractions can be non-trivial, as it requires both domain expertise and knowledge ab…
▽ More
Many example-guided program synthesis techniques use abstractions to prune the search space. While abstraction-based synthesis has proven to be very powerful, a domain expert needs to provide a suitable abstract domain, together with the abstract transformers of each DSL construct. However, coming up with useful abstractions can be non-trivial, as it requires both domain expertise and knowledge about the synthesizer. In this paper, we propose a new technique for learning abstractions that are useful for instantiating a general synthesis framework in a new domain. Given a DSL and a small set of training problems, our method uses tree interpolation to infer reusable predicate templates that speed up synthesis in a given domain. Our method also learns suitable abstract transformers by solving a certain kind of second-order constraint solving problem in a data-driven way. We have implemented the proposed method in a tool called ATLAS and evaluate it in the context of the BLAZE meta-synthesizer. Our evaluation shows that (a) ATLAS can learn useful abstract domains and transformers from few training problems, and (b) the abstractions learned by ATLAS allow BLAZE to achieve significantly better results compared to manually-crafted abstractions.
△ Less
Submitted 11 April, 2018;
originally announced April 2018.
-
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Authors:
Anvesh Komuravelli,
Nikolaj Bjorner,
Arie Gurfinkel,
Kenneth L. McMillan
Abstract:
We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely restricted to handling linear arithmetic operations and properties, or are non-compositional. We use Constrained Horn Clauses (CHCs) to represent the verification conditions where the memory operations are modeled using…
▽ More
We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely restricted to handling linear arithmetic operations and properties, or are non-compositional. We use Constrained Horn Clauses (CHCs) to represent the verification conditions where the memory operations are modeled using the extensional theory of arrays (ARR). First, we describe an exponential time quantifier elimination (QE) algorithm for ARR which can introduce new quantifiers of the index and value sorts. Second, we adapt the QE algorithm to efficiently obtain under-approximations using models, resulting in a polynomial time Model Based Projection (MBP) algorithm. Third, we integrate the MBP algorithm into the framework of compositional reasoning of procedural programs using may and must summaries recently proposed by us. Our solutions to the CHCs are currently restricted to quantifier-free formulas. Finally, we describe our practical experience over SV-COMP'15 benchmarks using an implementation in the tool SPACER.
△ Less
Submitted 6 August, 2015;
originally announced August 2015.
-
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
Authors:
Nikolaj Bjorner,
Ken McMillan,
Andrey Rybalchenko
Abstract:
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs directly as first-order SMT problems over Horn clauses. It is straight-forward to reduce Hoare-style verification of first-order programs into satisfiability of Horn clauses. The presence of closures offers several challen…
▽ More
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs directly as first-order SMT problems over Horn clauses. It is straight-forward to reduce Hoare-style verification of first-order programs into satisfiability of Horn clauses. The presence of closures offers several challenges: relatively complete proof systems have to account for closures; and in practice, the effectiveness of search procedures depend on encoding strategies and capabilities of underlying solvers. We here use algebraic data-types to encode closures and rely on solvers that support algebraic data-types. The viability of the approach is examined using examples from the literature on higher-order program verification.
△ Less
Submitted 21 June, 2013;
originally announced June 2013.
-
Interpolant-Based Transition Relation Approximation
Authors:
Ranjit Jhala,
Kenneth L. McMillan
Abstract:
In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given an adequate set of predicates. We present an interpolant-based method for strengthening the abstr…
▽ More
In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given an adequate set of predicates. We present an interpolant-based method for strengthening the abstract transition relation in case of such failures. This approach guarantees convergence given an adequate set of predicates, without requiring an exact image computation. We show empirically that the method converges more rapidly than an earlier method based on counterexample analysis.
△ Less
Submitted 1 November, 2007; v1 submitted 4 June, 2007;
originally announced June 2007.
