26,098 papers · page 84 of 1,305
In addition to requirements of a purely technical nature, the evolution of widely adopted programming languages is often governed by preferences of individual members---either persons or organizations---of the language maintenance team, who may associate issues with particular de…
Mobile devices have become integral to our everyday lives, yet their utility hinges on their battery life. In Android apps, resource leaks caused by inefficient resource management are a significant contributor to battery drain and poor user experience. Our work introduces Alpakk…
Fully general parsers permit the syntax specification of formal languages to be unrestricted, allowing language designers to use a syntax specification that supports semantics specification, but also permitting ambiguity. Language workbenches that support fully general grammars n…
In his 1977 ACM Turing Award Lecture, John Backus identified the word-at-a-time style of programming, inherited from the underlying hardware and dubbed the "von Neumann bottleneck", as a major obstacle to the advancement of programming. In this keynote, I argue that the functiona…
Abstract Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in using machine learning models in conjunction with proof assistants to per…
Abstract The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibil…
Abstract Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the…
Abstract Recent advances in satisfiability modulo theories have brought practical software verification within reach. The advent of the LLVM project presents a common representation which allows verification between programs written in different languages such as C and Rust. New …
Abstract Automatic decision and prediction systems are increasingly deployed in applications where they significantly impact the livelihood of people, such as for predicting the creditworthiness of loan applicants or the recidivism risk of defendants. These applications have give…
Abstract CPAchecker is a tool for software verification, witness validation, and test-case generation, based on the concept of configurable program analysis. One of its main applications is to validate correctness and violation witnesses in versions 1.0 and 2.0. The witness valid…
Abstract The 14th edition of the Competition on Software Verification (SV-COMP 2025) evaluated 62 verification tools and 18 witness validation tools, making it the largest comparison of its kind so far. Out of these, 35 verification and 13 validation tools participated with an ac…
Abstract Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automat…
Abstract Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results mo…
Abstract We study algorithms for solving parity, mean-payoff and energy games. We propose a systematic framework, which we call Fast value iteration, for describing, comparing, and proving correctness of such algorithms. The approach is based on potential reductions, as introduce…
Abstract We tackle the problem of enumerating set-theoretic solutions to the Yang-Baxter equation. This equation originates from statistical and quantum mechanics, but also has applications in knot theory, cryptography, quantum computation and group theory. Non-degenerate, involu…
Abstract Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize acceptance conditions of boolean $$\omega $$ ω -automata. Despite the theoretical advances …
Abstract Cooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together wi…
Abstract We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score…
Abstract Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic ap…
Abstract The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates —lightweight, easy-to-check proofs of the verificat…