| Description |
1 online resource (xiv, 528 pages) : illustrations (some color) |
| Series |
Lecture Notes in Computer Science, 0302-9743 ; 8172 |
|
LNCS sublibrary. SL 2, Programming and software engineering |
|
Lecture notes in computer science ; 8172.
|
|
LNCS sublibrary. SL 2, Programming and software engineering.
|
| Contents |
Invited Papers. Acceleration for Petri Nets / Jérôme Leroux -- Automated Verification and Strategy Synthesis for Probabilistic Systems / Marta Kwiatkowska, David Parker -- SMT-Based Software Model Checking / Alessandro Cimatti -- Regular Papers. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment / Tomáš Babiak ... et al. -- Improved Upper and Lower Bounds for Büchi Disambiguation / Hrishikesh Karmarkar, Manas Joglekar, Supratik Chakraborty -- Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points / Thomas Brihaye ... et al. -- An Automatic Technique for Checking the Simulation of Timed Systems / Elie Fares ... et al. -- Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games / Aleksandra Jovanović, Didier Lime, Olivier H. Roux -- Kleene Algebras and Semimodules for Energy Problems / Zoltán Ésik ... et al. -- Looking at Mean-Payoff and Total-Payoff through Windows / Krishnendu Chatterjee ... et al. -- Weighted Safety / Sigal Weiner ... et al. -- A Framework for Ranking Vacuity Results / Shoham Ben-David, Orna Kupferman |
|
Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications / Ramiro Demasi ... et al. -- Verification of a Dynamic Management Protocol for Cloud Applications / Rim Abid ... et al. -- Compact Symbolic Execution / Jiri Slaby, Jan Strejček, Marek Trtík -- Multi-threaded Explicit State Space Exploration with State Reconstruction / Sami Evangelista, Lars Michael Kristensen, Laure Petrucci -- Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata / Parosh Aziz Abdulla ... et al. -- Integrating Policy Iterations in Abstract Interpreters / Pierre Roux, Pierre-Loïc Garoche -- Interpolation Properties and SAT-Based Model Checking / Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina -- Analysis of Message Passing Programs Using SMT-Solvers / Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg -- An Expressive Framework for Verifying Deadlock Freedom / Duy-Khanh Le, Wei-Ngan Chin, Yong-Meng Teo -- Expected Termination Time in BPA Games / Dominik Wojtczak |
|
Precise Cost Analysis via Local Reasoning / Diego Esteban Alonso-Blas, Puri Arenas, Samir Genaim -- Control Flow Refinement and Symbolic Computation of Average Case Bound / Hong Yi Chen, Supratik Mukhopadhyay, Zheng Lu -- Termination and Cost Analysis of Loops with Concurrent Interleavings / Elvira Albert ... et al. -- Linear Ranking for Linear Lasso Programs / Matthias Heizmann ... et al. -- Merge and Conquer: State Merging in Parametric Timed Automata / Étienne André, Laurent Fribourg, Romain Soulat -- An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications / Orna Grumberg, Orna Kupferman, Sarai Sheinvald -- Pushdown Systems with Stack Manipulation / Yuya Uezato, Yasuhiko Minamide -- Robustness Analysis of String Transducers / Roopsha Samanta, Jyotirmoy V. Deshmukh, Swarat Chaudhuri -- Tool Papers. Manipulating LTL Formulas Using Spot 1.0 / Alexandre Duret-Lutz -- Rabinizer 2: Small Deterministic Automata for LTL\GU / Jan Křetínský, Ruslán Ledesma Garza -- LTL Model Checking with Neco / Łukasz Fronc, Alexandre Duret-Lutz |
|
Solving Parity Games on the GPU / Philipp Hoffmann, Michael Luttenberger -- PyEcdar: Towards Open Source Implementation for Timed Systems / Axel Legay, Louis-Marie Traonouez -- CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains / Yang Gao ... et al. -- NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems / Romain Testylier, Thao Dang -- CELL: A Compositional Verification Framework / Kun Ji ... et al. -- VCS: A Verifier for Component-Based Systems / Fei He ... et al. -- SmacC: A Retargetable Symbolic Execution Engine / Armin Biere ... et al. -- MoTraS: A Tool for Modal Transition Systems and Their Extensions / Jan Křetínský, Salomon Sickert -- Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs / César Rodríguez, Stefan Schwoon -- Short Papers. SAT Based Verification of Network Data Planes / Shuyuan Zhang, Sharad Malik -- A Theory for Control-Flow Graph Exploration / Stephan Arlt, Philipp Rümmer, Martin Schäf -- The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis / Jakob Mund ... et al |
| Summary |
This book constitutes the refereed proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, held at Hanoi, Vietnam, in October 2013. The 27 regular papers, 3 short papers and 12 tool papers presented together with 3 invited talks were carefully selected from 73 submissions. The papers are organized in topical, sections on analysis and verification of hardware circuits, systems-on-chip and embedded systems, analysis of real-time, hybrid, priced/weighted and probabilistic systems, deductive, algorithmic, compositional, and abstraction/refinement techniques for analysis and verification, analytical techniques for safety, security, and dependability, testing and runtime analysis based on verification technology, analysis and verification of parallel and concurrent hardware/software systems, verification in industrial practice, and applications and case studies |
| Analysis |
computerwetenschappen |
|
computer sciences |
|
programmeertalen |
|
programming languages |
|
programmeren |
|
programming |
|
software engineering |
|
operating systems |
|
computernetwerken |
|
computer networks |
|
Information and Communication Technology (General) |
|
Informatie- en communicatietechnologie (algemeen) |
| Notes |
International conference proceedings |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
Online resource; title from PDF title page (SpringerLink, viewed September 3, 2013) |
| Subject |
Automatic theorem proving -- Congresses
|
|
Artificial intelligence -- Congresses
|
|
Artificial intelligence.
|
|
Logic.
|
|
Artificial Intelligence
|
|
Logic
|
|
artificial intelligence.
|
|
logic.
|
|
Logic
|
|
Artificial intelligence
|
|
Automatic theorem proving
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Dang, Hung Van, 1950- editor.
|
|
Ogawa, Mizuhito, editor
|
| ISBN |
9783319024448 |
|
3319024442 |
|
