Abstract is missing.
- Scalable Timing Analysis with RefinementNan Guan, Yue Tang, Jakaria Abdullah, Martin Stigge, Wang Yi 0001. 3-18 [doi]
- A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance SystemJean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, André Platzer. 21-36 [doi]
- Verified Reachability Analysis of Continuous SystemsFabian Immler. 37-51 [doi]
- HyComp: An SMT-Based Model Checker for Hybrid SystemsAlessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. 52-67 [doi]
- C2E2: A Verification Tool for Stateflow ModelsParasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan 0001, Matthew Potok. 68-82 [doi]
- Non-cumulative Resource AnalysisElvira Albert, Jesús Correas Fernández, Guillermo Román-Díez. 85-100 [doi]
- Value Slice: A New Slicing Concept for Scalable Property CheckingShrawan Kumar, Amitabha Sanyal, Uday P. Khedker. 101-115 [doi]
- A Method for Improving the Precision and Coverage of Atomicity Violation PredictionsReng Zeng, Zhuo Sun, Su Liu, Xudong He. 116-130 [doi]
- Commutativity of ReducersYu-Fang Chen, Chih-Duo Hong, Nishant Sinha, Bow-Yaw Wang. 131-146 [doi]
- Inferring Simple Solutions to Recursion-Free Horn Clauses via SamplingHiroshi Unno, Tachio Terauchi. 149-163 [doi]
- Analysis of Dynamic Process NetworksKedar S. Namjoshi, Richard J. Trefler. 164-178 [doi]
- MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff ObjectivesTomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera. 181-187 [doi]
- syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic SpecificationsRamiro Demasi, Pablo F. Castro, Nicolás Ricci, Thomas Stephen Edward Maibaum, Nazareno Aguirre. 188-193 [doi]
- νZ - An Optimizing SMT SolverNikolaj Bjørner, Anh-Dung Phan, Lars Fleckenstein. 194-199 [doi]
- dReach: δ-Reachability Analysis for Hybrid SystemsSoonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke. 200-205 [doi]
- Uppaal StrategoAlexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis, Jakob Haahr Taankvist. 206-211 [doi]
- BINSEC: Binary Code Analysis with Low-Level RegionsAdel Djoudi, Sébastien Bardin. 212-217 [doi]
- Insight: An Open Binary Analysis FrameworkEmmanuel Fleury, Olivier Ly, Gérald Point, Aymeric Vincent. 218-224 [doi]
- SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification PlatformAlessandro Armando, Gianluca Bocci, Giantonio Chiarelli, Gabriele Costa, Gabriele De Maglie, Rocco Mammoliti, Alessio Merlo. 225-230 [doi]
- Symbolic Model-Checking Using ITS-ToolsYann Thierry-Mieg. 231-237 [doi]
- Semantic Importance Sampling for Statistical Model CheckingJeffery P. Hansen, Lutz Wrage, Sagar Chaki, Dionisio de Niz, Mark H. Klein. 241-255 [doi]
- Strategy Synthesis for Stochastic Games with Multiple Long-Run ObjectivesNicolas Basset, Marta Z. Kwiatkowska, Ufuk Topcu, Clemens Wiltsche. 256-271 [doi]
- 2 : Formal Abstractions of Uncountable-STate STochastic ProcessesSadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, Alessandro Abate. 272-286 [doi]
- Linearly Ordered Attribute Grammar Scheduling Using SAT-SolvingJeroen Bransen, L. Thomas van Binsbergen, Koen Claessen, Atze Dijkstra. 289-303 [doi]
- On Parallel Scalable Uniform SAT Witness GenerationSupratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi. 304-319 [doi]
- Approximate Counting in SMT and Value Estimation for Probabilistic ProgramsDmitry V. Chistikov, Rayna Dimitrova, Rupak Majumdar. 320-334 [doi]
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost FunctionsRoberto Sebastiani, Patrick Trentin. 335-349 [doi]
- Stateless Model Checking for TSO and PSOParosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos F. Sagonas. 353-367 [doi]
- GPU Accelerated Strong and Branching Bisimilarity CheckingAnton Wijs. 368-383 [doi]
- Fairness for Infinite-State SystemsByron Cook, Heidy Khlaaf, Nir Piterman. 384-398 [doi]
- Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015)Dirk Beyer 0001. 401-416 [doi]
- AProVE: Termination and Memory Safety of C Programs - (Competition Contribution)Thomas Ströder, Cornelius Aschermann, Florian Frohn, Jera Hensel, Jürgen Giesl. 417-419 [doi]
- Cascade - (Competition Contribution)Wei Wang, Clark Barrett. 420-422 [doi]
- CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution)Matthias Dangl, Stefan Löwe, Philipp Wendler. 423-425 [doi]
- CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution)Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang. 426-428 [doi]
- FramewORk for Embedded System verification - (Competition Contribution)Pablo González de Aledo, Pablo Sánchez Espeso. 429-431 [doi]
- Forester: Shape Analysis Using Tree Automata - (Competition Contribution)Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar. 432-435 [doi]
- MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution)Ermenegildo Tomasco, Omar Inverso, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 436-438 [doi]
- Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution)Franck Cassez, Takashi Matsuoka, Edward Pierzchalski, Nathan Smyth. 439-442 [doi]
- Predator Hunting Party (Competition Contribution)Petr Müller, Petr Peringer, Tomás Vojnar. 443-446 [doi]
- SeaHorn: A Framework for Verifying C Programs (Competition Contribution)Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas. 447-450 [doi]
- SMACK+Corral: A Modular Verifier - (Competition Contribution)Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric. 451-454 [doi]
- Ultimate Automizer with Array Interpolation - (Competition Contribution)Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Andreas Podelski. 455-457 [doi]
- ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution)Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, Andreas Podelski. 458-460 [doi]
- Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution)Truc L. Nguyen, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 461-463 [doi]
- FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution)Caterina Urban. 464-466 [doi]
- Model Checking Gene Regulatory NetworksMirco Giacobbe, Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Tiago Paixão, Tatjana Petrov. 469-483 [doi]
- Symbolic Quantitative Robustness Analysis of Timed AutomataOcan Sankur. 484-498 [doi]
- Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive SynthesisRajeev Alur, Salar Moarref, Ufuk Topcu. 501-516 [doi]
- Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial InformationRoderick Bloem, Krishnendu Chatterjee, Swen Jacobs, Robert Könighofer. 517-532 [doi]
- Shield Synthesis: - Runtime Enforcement for Reactive SystemsRoderick Bloem, Bettina Könighofer, Robert Könighofer, Chao Wang. 533-548 [doi]
- Verifying Concurrent Programs by Memory UnwindingErmenegildo Tomasco, Omar Inverso, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 551-565 [doi]
- AutoProof: Auto-Active Functional Verification of Object-Oriented ProgramsJulian Tschannen, Carlo A. Furia, Martin Nordio, Nadia Polikarpova. 566-580 [doi]
- An LTL Proof System for Runtime VerificationClare Cini, Adrian Francalanza. 581-595 [doi]
- MarQ: Monitoring at Runtime with QEAGiles Reger, Helena Cuenca Cruz, David E. Rydeheard. 596-610 [doi]
- Parallel Explicit Model Checking for Generalized Büchi AutomataEtienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud. 613-627 [doi]
- Limit Deterministic and Probabilistic Automata for LTL ∖ GUDileep Kini, Mahesh Viswanathan 0001. 628-642 [doi]
- Saturation-Based Incremental LTL Model Checking with Inductive ProofsVince Molnár, Dániel Darvas, András Vörös, Tamás Bartha. 643-657 [doi]
- Nested Antichains for WS1STomás Fiedor, Lukás Holík, Ondrej Lengál, Tomás Vojnar. 658-674 [doi]
- Sylvan: Multi-Core Decision DiagramsTom van Dijk, Jaco van de Pol. 677-691 [doi]
- LTSmin: High-Performance Language-Independent Model CheckingGijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, Tom van Dijk. 692-707 [doi]
- Using a Formal Model to Improve Verification of a Cache-Coherent System-on-ChipAbderahman Kriouile, Wendelin Serwe. 708-722 [doi]