Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs
Abstract elided by the publisher.
642 papers · page 28 of 33
Shape Analysis by Predicate Abstraction
Abstract elided by the publisher.
Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs
Abstract elided by the publisher.
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties
Abstract elided by the publisher.
Termination of Polynomial Programs
Abstract elided by the publisher.
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement
Abstract elided by the publisher.
Abstract Interpretation with Alien Expressions and Heap Structures
Abstract elided by the publisher.
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming
Abstract elided by the publisher.
Automata as Abstractions
Abstract elided by the publisher.
The Arithmetic-Geometric Progression Abstract Domain
We present a new numerical abstract domain. This domain automatically detects and proves bounds on the values of program variables. For that purpose, it relates variable values to a clock counter. More precisely, it bounds these values with the i-th iterate of the function [X↦α×X…
Information Flow Analysis for Java Bytecode
Abstract elided by the publisher.
Cryptographic Protocol Analysis on Real C Code
Abstract elided by the publisher.
Don't Know in the µ-Calculus
Abstract elided by the publisher.
The Verifying Compiler, a Grand Challenge for Computing Research
Abstract elided by the publisher.
Verification of an Error Correcting Code by Abstract Interpretation
Abstract elided by the publisher.
I/O Efficient Directed Model Checking
Abstract elided by the publisher.
On the Complexity of Error Explanation
Abstract elided by the publisher.
Generalized Typestate Checking for Data Structure Consistency
Abstract elided by the publisher.
Weak Automata for the Linear Time µ-Calculus
Abstract elided by the publisher.
Simple Is Better: Efficient Bounded Model Checking for Past LTL
Abstract elided by the publisher.