Proving the Existence of Fair Paths in Infinite-State Systems
Abstract elided by the publisher.
26,098 papers · page 310 of 1,305
Verification of Concurrent Programs Using Petri Net Unfoldings
Abstract elided by the publisher.
Model Checking Algorithms for Hyperproperties (Invited Paper)
Hyperproperties generalize trace properties by expressing relations between multiple computations. Hyperpropertes include policies from information-flow security, like observational determinism or non-interference, and many other system properties including promptness and knowled…
Compositional Model Checking for Multi-properties
Abstract elided by the publisher.
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
Abstract elided by the publisher.
Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)
Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our res…
GPURepair: Automated Repair of GPU Kernels
This paper presents a tool for repairing errors in GPU kernels written in CUDA or OpenCL due to data races and barrier divergence. Our novel extension to prior work can also remove barriers that are deemed unnecessary for correctness. We implement these ideas in our tool called G…
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
Abstract elided by the publisher.
Decomposing Data Structure Commutativity Proofs with $m\!n$-Differencing
Abstract elided by the publisher.
A Design of GPU-Based Quantitative Model Checking
Abstract elided by the publisher.
Compositional Satisfiability Solving in Separation Logic
Abstract elided by the publisher.
A Self-certifying Compilation Framework for WebAssembly
Abstract elided by the publisher.
Twinning Automata and Regular Expressions for String Static Analysis
Abstract elided by the publisher.
Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis
Abstract elided by the publisher.
On Preprocessing for Weighted MaxSAT
Abstract elided by the publisher.
Concurrent Correctness in Vector Space
Abstract elided by the publisher.
Unbounded Procedure Summaries from Bounded Environments
Abstract elided by the publisher.
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
Abstract elided by the publisher.
Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)
Abstract elided by the publisher.
Eliminating Message Counters in Synchronous Threshold Automata
Abstract elided by the publisher.