26,098 papers · page 141 of 1,305
The history of software development includes numerous tex- tual and graphical ways to represent software structures and the mechanisms for executing high-level instructions. The proliferation of programming languages is a visible outcome of that effort, with many popular language…
Orthogonal persistence implemented with non-volatile memory (NVM) allows the programmers to easily create persistent containers, which are container data-structures preserved even after the process terminations due to a system crash. However, the state-of-the-art technique of its…
Abstract We examine verification of concurrent programs under the total store ordering (TSO) semantics used by thex86architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show t…
Abstract Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts.Certifyingverifiers enhance the confidence in verification results by generating awitnessfor other tools to validate the verdict independently. Recently, tra…
Abstract Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. I…
Abstract We give an account of JPF’s current architecture as it has evolved over the last 20 years. Key changes include a modular, extensible design, and Java 11 support. Java 11 brought with it fundamental changes in the language and its runtime, in particular, a new modular lib…
Abstract Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a singlepolicyfulfills all objectives. We presentauction-based scheduling, adecentralizedframework for multi-objective s…
Abstract Witch 3 is a new validator of violation witnesses in the witness format 2.0. Note that our previous tool,Symbiotic-Witch 2, can validate only violation witnesses in the old GraphML format.Witch 3 validates witnesses of reachability of an error function, overflows, and in…
Abstract Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we…
Abstract CPAcheckeris a versatile framework for software verification, rooted in the established concept ofconfigurable program analysis. Compared to the last published system description at SV-COMP 2015, theCPAcheckersubmission to SV-COMP 2024 incorporates new analyses for reach…
Abstract ConcurrentWitness2Testis a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test …
Abstract Thetais a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led toThetabeing unable to meaningfully adapt. Identifying this probl…
Abstract Thetais a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3)…
Abstract In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort ( "Image missing") using the KeY program verification system. As "Image missing" is one of the fastest general purpose sorting algorithms, t…
Abstract Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification ofk-safety properties, i.e., properties that state that allk-tuples of execution traces sat…
Abstract The 13th edition of the Competition on Software Verification (SV-COMP 2024) was the largest competition of its kind so far: A total of 76 tools for verification and witness validation were compared. The competition evaluated 59 verification systems and 17 validation syst…
Abstract Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviours are described by session types. Asynchronous session subtyping is undecidable, hence the interest in devising …
Abstract Strategies for partially observable Markov decision processes (POMDP) typically require memory. One way to represent this memory is via automata. We present a method to learn an automaton representation of a strategy using a modification of the $$L^*$$ L ∗ -algorithm. Co…
Abstract Quadratization refers to a transformation of an arbitrary system of polynomial ordinary differential equations to a system with at most quadratic right-hand side. Such a transformation unveils new variables and model structures that facilitate model analysis, simulation,…
Abstract Bubaak-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top ofBubaak, a tool designed for running combinations of verifiers in parallel. In contrast toBubaak, that directly invokes verifiers on …