Approximate Counting in SMT and Value Estimation for Probabilistic Programs
Abstract elided by the publisher.
1,553 papers · page 38 of 78
HyComp: An SMT-Based Model Checker for Hybrid Systems
Abstract elided by the publisher.
An LTL Proof System for Runtime Verification
Abstract elided by the publisher.
Fairness for Infinite-State Systems
In this paper we introduce the first known tool for symbolically proving fair-CTL properties of infinite-state integer programs. Our solution is based on a reduction to existing techniques for fairness-free CTL model checking via the use of infinite non-deterministic branching to…
CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution)
Abstract elided by the publisher.
Uppaal Stratego
Abstract elided by the publisher.
syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
In this paper we introduce syntMaskFT, a tool that synthesizes fault-tolerant programs from specifications written in a fragment of branching time logic with deontic operators, designed for specifying fault-tolerant systems. The tool focuses on producing masking tolerant programs…
Sylvan: Multi-Core Decision Diagrams
Abstract elided by the publisher.
BINSEC: Binary Code Analysis with Low-Level Regions
Abstract elided by the publisher.
C2E2: A Verification Tool for Stateflow Models
Abstract elided by the publisher.
Nested Antichains for WS1S
Abstract elided by the publisher.
Insight: An Open Binary Analysis Framework
Abstract elided by the publisher.
Model Checking Gene Regulatory Networks
The behaviour of gene regulatory networks GRNs is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus…
Scalable Timing Analysis with Refinement
Abstract elided by the publisher.
SeaHorn: A Framework for Verifying C Programs (Competition Contribution)
Abstract elided by the publisher.
Semantic Importance Sampling for Statistical Model Checking
Abstract elided by the publisher.
SMACK+Corral: A Modular Verifier - (Competition Contribution)
Abstract elided by the publisher.
Ultimate Automizer with Array Interpolation - (Competition Contribution)
Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The i…
Forester: Shape Analysis Using Tree Automata - (Competition Contribution)
Abstract elided by the publisher.
Verified Reachability Analysis of Continuous Systems
Abstract elided by the publisher.