Sciweavers

CAV
2015
Springer
21views Hardware» more  CAV 2015»
8 years 8 months ago
The Hanoi Omega-Automata Format
We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simpl...
Tomás Babiak, Frantisek Blahoudek, Alexandr...
CAV
2015
Springer
22views Hardware» more  CAV 2015»
8 years 8 months ago
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki...
CAV
2015
Springer
18views Hardware» more  CAV 2015»
8 years 8 months ago
Deciding Local Theory Extensions via E-matching
Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automa...
Kshitij Bansal, Andrew Reynolds, Tim King 0001, Cl...
CAV
2015
Springer
28views Hardware» more  CAV 2015»
8 years 8 months ago
Algorithms for Model Checking HyperLTL and HyperCTL ^*
We present an automata-based algorithm for checking finite state systems for hyperproperties specified in HyperLTL and HyperCTL∗ . For the alternation-free fragments of HyperLT...
Bernd Finkbeiner, Markus N. Rabe, César S&a...
CAV
2015
Springer
20views Hardware» more  CAV 2015»
8 years 8 months ago
Fast Interpolating BMC
Abstract. Bounded Model Checking (BMC) is well known for its simplicity and ability to find counterexamples. It is based on the idea of symbolically representing counterexamples i...
Yakir Vizel, Arie Gurfinkel, Sharad Malik
CAV
2015
Springer
28views Hardware» more  CAV 2015»
8 years 8 months ago
Automata-Based Model Counting for String Constraints
Most common vulnerabilities in Web applications are due to string manipulation errors in input validation and sanitization code. String constraint solvers are essential components ...
Abdulbaki Aydin, Lucas Bang, Tevfik Bultan
CAV
2015
Springer
18views Hardware» more  CAV 2015»
8 years 8 months ago
Time-Aware Abstractions in HybridSal
re Abstractions in HybridSal Ashish Tiwari SRI International, Menlo Park, CA Abstract. HybridSal is a tool for enabling verification of hybrid systems using infinite bounded mode...
Ashish Tiwari
CAV
2015
Springer
15views Hardware» more  CAV 2015»
8 years 8 months ago
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
t). RECOMB/ISCB Conference on Regulatory and Systems Genomics, 2014 POPL 2013 Ali Sinan Köksal, Yewen Pu, Saurabh Srivastava, Rastislav Bodík, Jasmin Fisher, Nir Piterman. Synthe...
Jasmin Fisher, Ali Sinan Köksal, Nir Piterman...
CAV
2015
Springer
24views Hardware» more  CAV 2015»
8 years 8 months ago
Adam: Causality-Based Synthesis of Distributed Systems
Abstract. We present Adam, a tool for the automatic synthesis of distributed systems with multiple concurrent processes. For each process, an individual controller is synthesized t...
Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüd...
CAV
2015
Springer
18views Hardware» more  CAV 2015»
8 years 8 months ago
Measuring with Timed Patterns
We propose a declarative measurement specification language for quantitative performance evaluation of hybrid (discrete-continuous) systems based on simulation traces. We use time...
Thomas Ferrère, Oded Maler, Dejan Nickovic,...