Almost Event-Rate Independent Monitoring of Metric Temporal Logic
Abstract elided by the publisher.
1,553 papers · page 31 of 78
Software Verification with Validation of Results - (Report on SV-COMP 2017)
Abstract elided by the publisher.
RPP: Automatic Proof of Relational Properties by Self-composition
Abstract elided by the publisher.
Counterexample-Guided Refinement of Template Polyhedra
Abstract elided by the publisher.
Up-To Techniques for Weighted Systems
Abstract elided by the publisher.
Proving Termination Through Conditional Termination
We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine conditional termination proofs. Our key insight is that a co…
Rewriting-Based Runtime Verification for Alternation-Free HyperLTL
Abstract elided by the publisher.
JANI: Quantitative Model and Tool Interaction
Abstract elided by the publisher.
Long-Run Rewards for Markov Automata
Abstract elided by the publisher.
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations
Abstract elided by the publisher.
Skink: Static Analysis of Programs in LLVM Intermediate Representation - (Competition Contribution)
Abstract elided by the publisher.
Interpolation-Based GR(1) Assumptions Refinement
This paper considers the problem of assumptions refinement in the context of unrealizable specifications for reactive systems. We propose a new counterstrategy-guided synthesis approach for GR(1) specifications based on Craig’s interpolants. Our interpolation-based method identif…
Symbiotic 4: Beyond Reachability - (Competition Contribution)
Abstract elided by the publisher.
Directed Automated Memory Performance Testing
Abstract elided by the publisher.
autoCode4: Structural Controller Synthesis
Abstract elided by the publisher.
VeriAbs: Verification by Abstraction (Competition Contribution)
Abstract elided by the publisher.
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack…
Precise Widening Operators for Proving Termination by Abstract Interpretation
Abstract elided by the publisher.
Efficient Certified Resolution Proof Checking
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders…
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight al…