| Description |
1 online resource |
| Series |
Lecture notes in computer science, 0302-9743 ; 7795 |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 7795.
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
Markov Chains -- On-the-Fly Exact Computation of Bisimilarity Distances / Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare -- The Quest for Minimal Quotients for Probabilistic Automata / Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang -- LTL Model Checking of Interval Markov Chains / Michael Benedikt, Rastislav Lenhardt, James Worrell -- Termination -- Ramsey vs. Lexicographic Termination Proving / Byron Cook, Abigail See, Florian Zuleger -- Structural Counter Abstraction / Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey -- Quantifier Elimination -- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors / Ajith K. John, Supratik Chakraborty -- SAT/SMT -- The MathSAT5 SMT Solver / Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani -- Formula Preprocessing in MUS Extraction / Anton Belov, Matti Järvisalo, Joao Marques-Silva -- Proof Tree Preserving Interpolation / Jürgen Christ, Jochen Hoenicke, Alexander Nutz -- Asynchronous Multi-core Incremental SAT Solving / Siert Wieringa, Keijo Heljanko |
|
Games and Synthesis -- Model-Checking Iterated Games / Chung-Hao Huang, Sven Schewe, Farn Wang -- Synthesis from LTL Specifications with Mean-Payoff Objectives / Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin -- PRISM-games: A Model Checker for Stochastic Multi-Player Games / Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, Aistis Simaitis -- Process Algebra -- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus / Radu Mateescu, Gwen Salaün -- An Overview of the mCRL2 Toolset and Its Recent Advances / Sjoerd Cranen, Jan Friso Groote, Jeroen J.A. Keiren, Frank P.M. Stappers -- Pushdown Systems Boolean/Integer Programs -- Analysis of Boolean Programs / Patrice Godefroid, Mihalis Yannakakis -- Weighted Pushdown Systems with Indexed Weight Domains / Yasuhiko Minamide -- Underapproximation of Procedure Summaries for Integer Programs / Pierre Ganty, Radu Iosif, Filip Konečný -- Runtime Verification and Model Checking -- Runtime Verification Based on Register Automata / Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos |
|
Unbounded Model-Checking with Interpolation for Regular Language Constraints / Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte -- eVolCheck: Incremental Upgrade Checker for C / Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina -- Intertwined Forward-Backward Reachability Analysis Using Interpolants / Yakir Vizel, Orna Grumberg, Sharon Shoham -- Concurrency -- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures / Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík, Bengt Jonsson, Ahmed Rezine -- A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems / Alexander Linden, Pierre Wolper -- Learning and Abduction -- Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory / David H. White, Gerald Lüttgen -- Synthesis of Circular Compositional Program Proofs via Abduction / Boyang Li, Isil Dillig, Thomas Dillig, Ken McMillan, Mooly Sagiv -- Timed Automata -- As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty / Jean-François Kempf, Marius Bozga, Oded Maler |
|
Integer Parameter Synthesis for Timed Automata / Aleksandra Jovanović, Didier Lime, Olivier H. Roux -- Security and Access Control -- LTL Model-Checking for Malware Detection / Fu Song, Tayssir Touili -- Policy Analysis for Self-administrated Role-Based Access Control / Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato -- Model Checking Agent Knowledge in Dynamic Access Control Policies / Masoud Koleini, Eike Ritter, Mark Ryan -- Frontiers (Graphics and Quantum) -- Automatic Testing of Real-Time Graphics Systems / Robert Nagy, Gerardo Schneider, Aram Timofeitchik -- Equivalence Checking of Quantum Protocols / Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan -- Functional Programs and Types -- Encoding Monomorphic and Polymorphic Types / Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone -- Deriving Probability Density Functions from Probabilistic Functional Programs / Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio Russo -- Tool Demonstrations |
|
Polyglot: Systematic Analysis for Multiple Statechart Formalisms / Daniel Balasubramanian, Corina S. Păsăreanu, Gábor Karsai, Michael R. Lowry -- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO / Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine -- BULL: A Library for Learning Algorithms of Boolean Functions / Yu-Fang Chen, Bow-Yaw Wang -- AppGuard -- Enforcing User Requirements on Android Apps / Michael Backes, Sebastian Gerling, Christian Hammer, Matteo Maffei -- Explicit-State Model Checking -- Model Checking Database Applications / Milos Gligoric, Rupak Majumdar -- Efficient Property Preservation Checking of Model Refinements / Anton Wijs, Luc Engelen -- Büchi Automata -- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking / Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud -- Competition on Software Verification -- Second Competition on Software Verification / Dirk Beyer |
|
CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation / Stefan Löwe -- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis / Philipp Wendler -- CSeq: A Sequentialization Tool for C / Bernd Fischer, Omar Inverso, Gennaro Parlato -- Handling Unbounded Loops with ESBMC 1.20 / Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer -- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM / Stephan Falke, Florian Merz, Carsten Sinz -- Predator: A Tool for Verification of Low-Level List Manipulation / Kamil Dudka, Petr Müller, Petr Peringer, Tomáš Vojnar -- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution / Jiri Slaby, Jan Strejček, Marek Trtík -- Threader: A Verifier for Multi-threaded Programs / Corneliu Popeea, Andrey Rybalchenko -- UFO: Verification with Interpolants and Abstract Interpretation / Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik -- Ultimate Automizer with SMTInterpol / Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke |
| Summary |
This book constitutes the proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, held in Rome, Italy, in March 2013. The 42 papers presented in this volume were carefully reviewed and selected from 172 submissions. They are organized in topical sections named: Markov chains; termination; SAT/SMT; games and synthesis; process algebra; pushdown; runtime verification and model checking; concurrency; learning and abduction; timed automata; security and access control; frontiers (graphics and quantum); functional programs and types; tool demonstrations; explicit-state model checking; Büchi automata; and competition on software verification |
| Analysis |
Computer science |
|
Software engineering |
|
Computer software |
|
Logic design |
|
Logics and Meanings of Programs |
|
Algorithm Analysis and Problem Complexity |
|
Programming Languages, Compilers, Interpreters |
|
computerwetenschappen |
|
computer sciences |
|
algoritmen |
|
algorithms |
|
computeranalyse |
|
computer analysis |
|
programmeertalen |
|
programming languages |
|
Information and Communication Technology (General) |
|
Informatie- en communicatietechnologie (algemeen) |
| Notes |
International conference proceedings |
| Bibliography |
Includes bibliographical references and author index |
| Subject |
System design -- Congresses
|
|
Computer software -- Verification -- Congresses
|
|
System analysis -- Congresses
|
|
Computer systems.
|
|
Computer software -- Validation.
|
|
Computer programs -- Validation.
|
|
System analysis.
|
|
Computer Systems
|
|
Software Validation
|
|
Systems Analysis
|
|
systems analysis.
|
|
Computer systems
|
|
Computer software -- Validation
|
|
Computer programs -- Validation
|
|
Computer software -- Verification
|
|
System analysis
|
|
System design
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Software.
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Piterman, Nir.
|
|
Smolka, Scott A.
|
|
ETAPS (Conference) (16th : 2013 : Rome, Italy)
|
| ISBN |
9783642367427 |
|
3642367429 |
|
3642367410 |
|
9783642367410 |
|
