| Description |
1 online resource |
| Series |
Lecture notes in computer science, 0302-9743 ; 7561 |
|
LNCS sublibrary. SL 2, Programming and software engineering |
|
Lecture notes in computer science ; 7561.
|
|
LNCS sublibrary. SL 2, Programming and software engineering.
|
| Contents |
Verification of Computer Switching Networks: An Overview / Shuyuan Zhang, Sharad Malik and Rick McGeer -- Dynamic Bayesian Networks: A Factored Model of Probabilistic Dynamics / Sucheendra K. Palaniappan and P.S. Thiagarajan -- Interpolant Automata (Invited Talk) / Andreas Podelski -- Approximating Deterministic Lattice Automata / Shulamit Halamish and Orna Kupferman -- Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata / Sven Schewe and Thomas Varghese -- A Succinct Canonical Register Automaton Model for Data Domains with Binary Relations / Sofia Cassel, Bengt Jonsson, Falk Howar and Bernhard Steffen -- Rabinizer: Small Deterministic Automata for LTL(F, G) / Andreas Gaiser, Jan Křetínský and Javier Esparza -- The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints / Paritosh K. Pandya and Simoni S. Shah |
|
On Temporal Logic and Signal Processing / Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic and Radu Grosu, et al. -- Improved Single Pass Algorithms for Resolution Proof Reduction / Ashutosh Gupta -- Model Checking Systems and Specifications with Parameterized Atomic Propositions / Orna Grumberg, Orna Kupferman and Sarai Sheinvald -- Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations / Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang and Antoine Girard -- Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding / Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar and Prakash Saivasan -- Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data / Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighireanu -- A Verifier for Functional Properties of Sequence-Manipulating Programs / Carlo A. Furia -- Accelerating Interpolants / Hossein Hojjat, Radu Iosif, Filip Konečný, Viktor Kuncak and Philipp Rümmer |
|
FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization / Ondrej Sery, Grigory Fedyukovich and Natasha Sharygina -- Synthesis of Succinct Systems / John Fearnley, Doron Peled and Sven Schewe -- Controllers with Minimal Observation Power (Application to Timed Systems) / Peter Bulychev, Franck Cassez, Alexandre David, Kim Guldstrand Larsen and Jean-François Raskin, et al. -- Counterexample Guided Synthesis of Monitors for Realizability Enforcement / Matthias Güdemann, Gwen Salaün and Meriem Ouederni -- Parallel Assertions for Architectures with Weak Memory Models / Daniel Schwartz-Narbonne, Georg Weissenbacher and Sharad Malik -- Improved Multi-Core Nested Depth-First Search / Sami Evangelista, Alfons Laarman, Laure Petrucci and Jaco van de Pol -- An Experiment on Parallel Model Checking of a CTL Fragment / Rodrigo T. Saad, Silvano Dal Zilio and Bernard Berthomieu -- Variable Probabilistic Abstraction Refinement / Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns and Björn Wachter |
|
Pareto Curves for Probabilistic Model Checking / Vojtěch Forejt, Marta Kwiatkowska and David Parker -- Verification of Partial-Information Probabilistic Systems Using Counterexample-Guided Refinements / Sergio Giro and Markus N. Rabe -- The COMICS Tool -- Computing Minimal Counterexamples for DTMCs / Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer and Joost-Pieter Katoen, et al. -- Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers / Daniel Neider -- ALLQBF Solving by Computational Learning / Bernd Becker, Rüdiger Ehlers, Matthew Lewis and Paolo Marin -- Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games / Krishnendu Chatterjee, Martin Chmelík and Rupak Majumdar -- A Probabilistic Kleene Theorem / Benedikt Bollig, Paul Gastin, Benjamin Monmege and Marc Zeitoun -- Higher-Order Approximations for Verification of Stochastic Hybrid Systems / Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate |
| Summary |
This book constitutes the thoroughly refereed proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, held at Thiruvananthapuram, Kerala, India, in October 2012. The 25 regular papers, 3 invited papers and 4 tool papers presented were carefully selected from numerous submissions. Conference papers are organized in 9 technical sessions, covering the topics of automata theory, logics and proofs, model checking, software verification, synthesis, verification and parallelism, probabilistic verification, constraint solving and applications, and probabilistic systems |
| Analysis |
Computer science |
|
Computer Communication Networks |
|
Software engineering |
|
Logic design |
|
Programming Techniques |
|
Logics and Meanings of Programs |
|
Programming Languages, Compilers, Interpreters |
|
Software Engineering/Programming and Operating Systems |
|
computerwetenschappen |
|
computer sciences |
|
programmeertalen |
|
programming languages |
|
programmeren |
|
programming |
|
operating systems |
|
computernetwerken |
|
computer networks |
|
Information and Communication Technology (General) |
|
Informatie- en communicatietechnologie (algemeen) |
| Bibliography |
Includes bibliographical references and author index |
| Subject |
Automatic theorem proving -- Congresses
|
|
Artificial intelligence -- Congresses
|
|
Informatique.
|
|
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 |
Chakraborty, Supratik
|
|
Mukund, Madhavan.
|
| ISBN |
9783642333866 |
|
3642333869 |
|
3642333850 |
|
9783642333859 |
|
