2,069 papers · page 19 of 104
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
Abstract We revisit two well-established verification techniques,k-inductionandbounded model checking(BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution islatticed k-induction, which (i) generalizes classicalk-inducti…
Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez
Abstract Hyperpropertiesare properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The te…
Sam Bayless, John D. Backes, Dan DaCosta, Benjamin F. Jones, Nate Launchbury, Patrick Trentin, Kelsey Jewell, Sagar Joshi + 2 more
Abstract In this industrial case study we describe a new network troubleshooting analysis used by VPC Reachability Analyzer , an SMT-based network reachability analysis and debugging tool. Our troubleshooting analysis uses a formal model of AWS Virtual Private Cloud (VPC) semanti…
Jaroslav Bendík, Kuldeep S. Meel
Abstract Given an unsatisfiable Boolean formulaFin CNF, an unsatisfiable subset of clauses U ofFis called Minimal Unsatisfiable Subset (MUS) if every proper subset ofUis satisfiable. Since MUSes serve as explanations for the unsatisfiability ofF, MUSes find applications in a wide…
Nikola Benes, Lubos Brim, Samuel Pastva, David Safránek
Abstract Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out o…
Freark I. van der Berg
Abstract Multi-threaded unit tests for high-performance thread-safe data structures typically do not test all behaviour, because only a single scheduling of threads is witnessed per invocation of the unit tests. Model checking such unit tests allows to verify all interleavings of…
Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, Vijay Ganesh
Abstract We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insi…
Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, Andrei Stefanescu
Abstract We have completed machine-assisted proofs of two highly-optimized cryptographic primitives, AES-256-GCM and SHA-384. We have verified that the implementations of these primitives, written in a mix of C and x86 assembly, are memory safe and functionally correct, by which …
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonás, Greg Kimberly
Abstract The process of developing civil aircraft and their related systems includes multiple phases of Preliminary Safety Assessment (PSA). An objective of PSA is to link the classification of failure conditions and effects (produced in the functional hazard analysis phases) to …
Nate F. F. Bragg, Jeffrey S. Foster, Cody Roux, Armando Solar-Lezama
Abstract Sketch is a popular program synthesis tool that solves for unknowns in a sketch or partial program. However, while Sketch is powerful, it does not directly support modular synthesis of dependencies, potentially limiting scalability. In this paper, we introduce Sketcham, …
Claudia Cauli, Meng Li, Nir Piterman, Oksana Tkachuk
Abstract Over the past ten years, the adoption of cloud services has grown rapidly, leading to the introduction of automated deployment tools to address the scale and complexity of the infrastructure companies and users deploy. Without the aid of automation, ensuring the security…
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
Abstract We present a novel verification technique to prove properties of a class of array programs with a symbolic parameter N denoting the size of arrays. The technique relies on constructing two slightly different versions of the same program. It infers difference relations be…
Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic
Abstract We introduce new algorithms for computing non-termination sensitive control dependence (NTSCD) and decisive order dependence (DOD). These relations on vertices of a control flow graph have many applications including program slicing and compiler optimizations. Our algori…
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu
Abstract We pursue the vision of anideal language framework, where programming language designers only need to define the formalsyntaxandsemanticsof their languages, and all language tools are automatically generated by the framework. Due to the complexity of such a language fram…
Michele Chiari, Dino Mandrioli, Matteo Pradella
Abstract The problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the lo…
Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A. Navas, Valentin Wüstholz
Abstract State-of-the-art program-analysis techniques are not yet able to effectively verify safety properties of heterogeneous systems, that is, systems with components implemented using diverse technologies. This shortcoming is pinpointed by programs invoking neural networks de…
Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong, Hannah Zicarelli
Abstract GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing approaches produce too m…
George A. Constantinides, Fredrik Dahlqvist, Zvonimir Rakamaric, Rocco Salvia
Abstract We present a detailed study of roundoff errors in probabilistic floating-point computations. We derive closed-form expressions for the distribution of roundoff errors associated with a random variable, and we prove that roundoff errors are generally close to being uncorr…
Loris D'Antoni, Qinheping Hu, Jinwoo Kim, Thomas W. Reps
Abstract Program synthesis is now a reality, and we are approaching the point where domain-specific synthesizers can now handle problems of practical sizes. Moreover, some of these tools are finding adoption in industry. However, for synthesis to become a mainstream technique ado…
Marco Eilers, Severin Meier, Peter Müller
Abstract Most existing program verifiers check trace properties such as functional correctness, but do not support the verification of hyperproperties, in particular, information flow security. In principle, product programs allow one to reduce the verification of hyperproperties…