From Shape Analysis to Termination Analysis in Linear Time
Abstract elided by the publisher.
26,098 papers · page 497 of 1,305
PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
Abstract elided by the publisher.
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
Abstract elided by the publisher.
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers
Abstract elided by the publisher.
Counterexample Guided Abstraction Refinement for Stability Analysis
Abstract elided by the publisher.
End-to-End Verification of Processors with ISA-Formal
Abstract elided by the publisher.
Probabilistic Automated Language Learning for Configuration Files
Abstract elided by the publisher.
BigraphER: Rewriting and Analysis Engine for Bigraphs
Abstract elided by the publisher.
Limit-Deterministic Büchi Automata for Linear Temporal Logic
Abstract elided by the publisher.
Progressive Reasoning over Recursively-Defined Strings
Abstract elided by the publisher.
String Analysis via Automata Manipulation with Logic Circuit Representation
Abstract elided by the publisher.
BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs
Abstract elided by the publisher.
A Practical Verification Framework for Preemptive OS Kernels
Abstract elided by the publisher.
Under-Approximating Backward Reachable Sets by Polytopes
Abstract elided by the publisher.
Iguana: a practical data-dependent parsing framework
Data-dependent grammars extend context-free grammars with arbitrary computation, variable binding, and constraints. These features provide the user with the freedom and power to express syntactic constructs outside the realm of context-free grammars, e.g., indentation rules in Ha…
SYCO: a systematic testing tool for concurrent objects
We present the concepts, usage and prototypical implementation of SYCO: a SYstematic testing tool for Concurrent Objects. The system receives as input a program, a selection of method to be tested, and a set of initial values for its parameters. SYCO offers a visual web interface…
Mapping deviation: a technique to adapt or to guard loop transformation intuitions for legality
Parallel architectures are now omnipresent in mainstream electronic devices and exploiting them efficiently is a challenge for all developers. Hence, they need the support of languages, libraries and tools to assist them in the optimization or parallelization task. Compilers can …
Verified construction of static single assignment form
Modern compilers use intermediate representations in static single assignment (SSA) form, which simplifies many optimizations. However, the high implementation complexity of efficient SSA construction algorithms poses a challenge to verified compilers. In this paper, we consider …
Restrictification of function arguments
Pointer aliasing still hinders compiler optimizations, in spite of years of research on pointer disambiguation. Because the automatic disambiguation of pointers is a difficult endeavor, several programming languages offer programmers mechanisms to distinguish memory references, s…
Reducing memory buffering overhead in software thread-level speculation
Software-based, automatic parallelization through Thread-Level Speculation (TLS) has significant practical potential, but also high overhead costs. Traditional "lazy" buffering mechanisms enable strong isolation of speculative threads, but imply large memory overheads, while more…