Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Abstract elided by the publisher.
26,098 papers · page 357 of 1,305
Cheap CTL Compassion in NuSMV
Abstract elided by the publisher.
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Abstract elided by the publisher.
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of inductive quantified loop invariants which, in some cases, may not even be first-order expressible. In this paper, we suggest a novel verification technique…
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specific…
A Systematic Approach to Abstract Interpretation of Program Transformations
Abstract elided by the publisher.
Improving Parity Game Solvers with Justifications
Abstract elided by the publisher.
Solving $\mathrm {LIA} ^\star $ Using Approximations
Abstract elided by the publisher.
Systematic Classification of Attackers via Bounded Model Checking
In this work, we study the problem of verification of systems in the presence of attackers using bounded model checking. Given a system and a set of security requirements, we present a methodology to generate and classify attackers, mapping them to the set of requirements that th…
Witnessing Secure Compilation
Compiler optimizations are designed to improve run-time performance while preserving input-output behavior. Correctness in this sense does not necessarily preserve security: it is known that standard optimizations may break or weaken security properties that hold of the source pr…
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
Abstract elided by the publisher.
Fixing Code that Explodes Under Symbolic Evaluation
Abstract elided by the publisher.
How to Win First-Order Safety Games
First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these sy…
Generalized Property-Directed Reachability for Hybrid Systems
Generalized property-directed reachability (GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification; for example, it is the core of Spacer, a state-of-the-art Horn-clause solver bundled with Z3. Howeve…
Synthesizing Environment Invariants for Modular Hardware Verification
Abstract elided by the publisher.
Assessing the quality of evolving Haskell systems by measuring structural inequality
Software metrics are used to measure the quality of a software system, and to understand the evolution of the system's quality over time. In this paper we report on an empirical study that investigates whether structural degradation in Haskell systems is related to decreasing sof…
Stitch: the sound type-indexed type checker (functional pearl)
A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC's bells and whistles. The Stitch interpre…
Scripted signal functions
Programming time-dependent signals like animations involves expressing both continuous and discrete changes in signal values. The method of functional reactive programming (FRP) represents this simply and effectively as discrete modes of an otherwise continuous signal. In variant…
Describing microservices using modern Haskell (experience report)
We present Mu, a domain specific language to describe and develop microservices in Haskell. At its core, Mu provides a type level representation of schemas, which we leverage in various ways. These schemas can be automatically imported from industry-standard interface definition …
Type your matrices for great good: a Haskell library of typed matrices and applications (functional pearl)
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithm…