Time for Statistical Model Checking of Real-Time Systems
Abstract elided by the publisher.
2,069 papers · page 53 of 104
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
Predicate abstraction is a key enabling technology for applying finitestate model checkers to programs written in mainstream languages. It has been used very successfully for debugging sequential system-level C code. Although model checking was originally designed for analyzing c…
Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
Abstract elided by the publisher.
SpaceEx: Scalable Verification of Hybrid Systems
Abstract elided by the publisher.
HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection
Abstract elided by the publisher.
From Cardiac Cells to Genetic Regulatory Networks
Abstract elided by the publisher.
Threader: A Constraint-Based Verifier for Multi-threaded Programs
Abstract elided by the publisher.
Interactive Synthesis of Code Snippets
Abstract elided by the publisher.
Forest Automata for Verification of Heap Manipulation
Abstract elided by the publisher.
Model Checking Recursive Programs with Numeric Data Types
Abstract elided by the publisher.
Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints
Abstract elided by the publisher.
μZ- An Efficient Engine for Fixed Points with Constraints
Abstract elided by the publisher.
Using Types for Software Verification
Abstract elided by the publisher.
HMC: Verifying Functional Programs Using Abstract Interpreters
We present Hindley-Milner-Cousots (HMC), an algorithm that reduces verification of safety properties of typed higher-order functional programs to interprocedural analysis for first-order imperative programs. HMC works as follows. First, it uses the type structure of the functiona…
A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations
Abstract elided by the publisher.
Bug-Assist: Assisting Fault Localization in ANSI-C Programs
Abstract elided by the publisher.
Synthesis of Distributed Control through Knowledge Accumulation
Abstract elided by the publisher.
Language Equivalence for Probabilistic Automata
Abstract elided by the publisher.
Formalization and Automated Verification of RESTful Behavior
Abstract elided by the publisher.
Linear Completeness Thresholds for Bounded Model Checking
Abstract elided by the publisher.