Synthesizing Ranking Functions from Bits and Pieces
Abstract elided by the publisher.
1,553 papers · page 37 of 78
Some Complexity Results for Stateful Network Verification
Abstract elided by the publisher.
Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication
Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 has been complied with by mainstream separation kernels. Security of functionalities defined in ARINC …
CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution)
Abstract elided by the publisher.
Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015)
Abstract elided by the publisher.
Stateless Model Checking for TSO and PSO
Abstract elided by the publisher.
Non-cumulative Resource Analysis
Abstract elided by the publisher.
FramewORk for Embedded System verification - (Competition Contribution)
Abstract elided by the publisher.
Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
Abstract elided by the publisher.
SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
Abstract elided by the publisher.
Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
Abstract elided by the publisher.
νZ - An Optimizing SMT Solver
Abstract elided by the publisher.
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
Synthesis of program parts is particularly useful for concurrent systems. However, most approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis AGS provides robustness ag…
Shield Synthesis: - Runtime Enforcement for Reactive Systems
Scalability issues may prevent users from verifying critical properties of a complex hardware design. In this situation, we propose to synthesize a "safety shield" that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model check…
Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving
Abstract elided by the publisher.
MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives
We present MultiGain, a tool to synthesize strategies for Markov decision processes MDPs with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for…
Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution)
Abstract elided by the publisher.
On Parallel Scalable Uniform SAT Witness Generation
Abstract elided by the publisher.
Commutativity of Reducers
Abstract elided by the publisher.
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution)
Abstract elided by the publisher.