1,553 papers · page 14 of 78
Roland Meyer, Thomas Wies, Sebastian Wolff
Abstract We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vanishing flows, and has …
Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
Abstract Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem. Unlike sequential solvers, however, distributed solvers have…
Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
Abstract Mopsa is a multilanguage static analysis platform relying on abstract interpretation. It is able to analyze C, Python, and programs mixing these two languages; we focus on the C analysis here. It provides a novel way to combine abstract domains, in order to offer extensi…
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
Abstract Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs …
Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugster, Natasha Sharygina
Abstract The need to provide formal guarantees about the behaviour of the algorithms underpinning modern distributed systems became evident in recent years. This interest made apparent the complexities involved in applying verification techniques in a distributed setting, with si…
Seung Hoon Park, Rekha R. Pai, Tom Melham
Abstract CHERI-C extends the C programming language by adding hardware capabilities , ensuring a certain degree of memory safety while remaining efficient. Capabilities can also be employed for higher-level security measures, such as software compartmentalization, that have to be…
Joseph E. Reeves, Benjamin Kiesl-Reiter, Marijn J. H. Heule
Abstract Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the well-known DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for s…
Simmo Saan, Michael Schwarz, Julian Erhard, Manuel Pietsch, Helmut Seidl, Sarah Tilscher, Vesal Vojdani
Abstract The static analyzer Goblint is dedicated to the analysis of multi-threaded C programs by abstract interpretation. It provides multiple techniques for increasing analysis precision, e.g., configurable context-sensitivity and a wide range of numerical analyses. As a rule o…
Ocan Sankur
Abstract We present algorithms for model checking and controller synthesis of timed automata, seeing a timed automaton model as a parallel composition of a large finite-state machine and a relatively smaller timed automaton, and using compositional reasoning on this composition. …
Yahui Song, Wei-Ngan Chin
Abstract The correctness of real-time systems depends both on the correct functionalities and the realtime constraints. To go beyond the existing Timed Automata based techniques, we propose a novel solution that integrates a modular Hoare-style forward verifier with a term rewrit…
Jie Su, Zuchao Yang, Hengrui Xing, Jiyu Yang, Cong Tian, Zhenhua Duan
Abstract is a tool for verifying reachability properties of concurrent C programs. It moderates the trace-space explosion problem, aggravated by thread alternation, through utilizing the PC-DPOR and C-Intp techniques. The PC-DPOR technique constructs a constrained dependency grap…
Bernardo Subercaseaux, Marijn J. H. Heule
Abstract A packing k -coloring is a natural variation on the standard notion of graph k -coloring, where vertices are assigned numbers from $$\{1, \ldots , k\}$$ { 1 , … , k } , and any two vertices assigned a common color $$c \in \{1, \ldots , k\}$$ c ∈ { 1 , … , k } need to be …
Bastien Thomas, Ocan Sankur
Abstract We present the tool PyLTA, which can model check parameterized distributed algorithms against LTL specifications. The parameters typically include the number of processes and a bound on faulty processes, and the considered algorithms are round-based and either synchronou…
Marck van der Vegt, Nils Jansen, Sebastian Junges
Abstract Multiple-environment MDPs (MEMDPs) capture finite sets of MDPs that share the states but differ in the transition dynamics. These models form a proper subclass of partially observable MDPs (POMDPs). We consider the synthesis of policies that robustly satisfy an almost-su…
Petar Vukmirovic, Jasmin Blanchette, Stephan Schulz
Abstract Most users of proof assistants want more proof automation. Some proof assistants discharge goals by translating them to first-order logic and invoking an efficient prover on them, but much is lost in translation. Instead, we propose to extend first-order provers with nat…
Yuning Wang, He Zhu
Abstract We present a verification-based learning framework VEL that synthesizes safe programmatic controllers for environments with continuous state and action spaces. The key idea is the integration of program reasoning techniques into controller training loops. VEL performs ab…
Anton Wijs, Muhammad Osama
Abstract Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to st…
Tobias Winkler, Joost-Pieter Katoen
Abstract Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem o…
Shengping Xiao, Chengyu Zhang, Jianwen Li, Geguang Pu
Abstract We present , a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one…
Zsófia Ádám, Levente Bajczi, Mihály Dobos-Kovács, Ákos Hajdu, Vince Molnár
Abstract Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non…