close
1.

図書

図書
Javier Esparza, Charles Lakos (eds.)
出版情報: Berlin : Springer, c2002  x, 444 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2360
所蔵情報: loading…
2.

電子ブック

EB
Javier Esparza, Keijo Heljanko
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2008
所蔵情報: loading…
目次情報: 続きを見る
Introduction / 1:
Transition Systems and Products / 2:
Transition Systems / 2.1:
Products of Transition Systems / 2.2:
Petri Net Representation of Products / 2.3:
Interleaving Representation of Products / 2.4:
Unfolding Products / 3:
Branching Processes and Unfoldings / 3.1:
Some Properties of Branching Processes / 3.2:
Branching Processes Are Synchronizations of Trees / 3.2.1:
Causality, Conflict, and Concurrency / 3.2.2:
Configurations / 3.2.3:
Verification Using Unfoldings / 3.3:
Constructing the Unfolding of a Product / 3.4:
Search Procedures / 3.5:
Goals and Milestones for Next Chapters / 3.6:
Search Procedures for the Executability Problem / 4:
Search Strategies for Transition Systems / 4.1:
Search Scheme for Transition Systems / 4.2:
Search Strategies for Products / 4.3:
Mazurkiewicz Traces / 4.3.1:
Search Strategies as Orders on Mazurkiewicz Traces / 4.3.2:
Search Scheme for Products / 4.4:
Counterexample to Completeness / 4.4.1:
Adequate Search Strategies / 4.5:
The Size and Parikh Strategies / 4.5.1:
Distributed Strategies / 4.5.2:
Complete Search Scheme for Arbitrary Strategies / 4.6:
More on the Executability Problem / 5:
Complete Prefixes / 5.1:
Some Complexity Results / 5.1.1:
Reducing Verification Problems to SAT / 5.1.2:
Least Representatives / 5.2:
Breadth-First and Depth-First Strategies / 5.3:
Total Breadth-First Strategies / 5.3.1:
Total Depth-First Strategies / 5.3.2:
Strategies Preserved by Extensions Are Well-Founded / 5.4:
Search Procedures for the Repeated Executability Problem / 6:
Search Procedures for the Livelock Problem / 6.1:
Model Checking LTL / 7.1:
Linear Temporal Logic / 8.1:
Interpreting LTL on Products / 8.2:
Extending the Interpretation / 8.2.1:
Testers for LTL Properties / 8.3:
Constructing a Tester / 8.3.1:
Model Checking with Testers: A First Attempt / 8.4:
Stuttering Synchronization / 8.5:
Summary, Applications, Extensions, and Tools / 9:
Looking Back: A Two-Page Summary of This Book / 9.1:
Some Experiments / 9.2:
Some Applications / 9.3:
Some Extensions / 9.4:
Some Tools / 9.5:
References
Index
Introduction / 1:
Transition Systems and Products / 2:
Transition Systems / 2.1:
3.

電子ブック

EB
Javier Esparza, Takeo Kanade, Rupak Majumdar
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2010
所蔵情報: loading…
目次情報: 続きを見る
Invited Talks
Embedded Systems Design - Scientific Challenges and Work Directions (Abstract) / Joseph Sifakis
Antichain Algorithms for Finite Automata / Laurent Doyen ; Jean-François Raskin
Probabilistic Systems and Optimization
Assume-Guarantee Verification for Probabilistic Systems / Marta Kwiatkowska ; Gethin Norman ; David Parker ; Hongyang Qu
Simple O(m log n) Time Markov Chain Lumping / Antti Valmari ; Giuliana Franceschinis
Model Checking Interactive Markov Chains / Lijun Zhang ; Martin R. Neuhäu?er
Approximating the Pareto Front of Multi-criteria Optimization Problems / Julien Legriel ; Colas Le Guernic ; Scott Cotton ; Oded Maler
Decision Procedures
An Alternative to SAT-Based Approaches for Bit-Vectors / Sébastien Bardin ; Philippe Herrmann ; Florian Perroud
Satisfiability Modulo the Theory of Costs: Foundations and Applications / Alessandro Cimatti ; Anders Franzén ; Alberto Griggio ; Roberto Sebastiani ; Cristian Stenico
Optimal Tableau Algorithms for Coalgebraic Logics / Rajeev Goré ; Clemens Kupke ; Dirk Pattinson
Blocked Clause Elimination / Matti Järvisalo ; Armin Biere ; Marijn Heule
Tools I
BOOM: Taking Boolean Program Model Checking One Step Further / Gerard Basler, Matthew Hague ; Daniel Kroening ; C.-H. Luke Ong ; Thomas Wahl ; Haoxian Zhao
The OpenSMT Solver / Roberto Bruttomesso ; Edgar Pek ; Natasha Sharygina ; Aliaksei Tsitovich
STRANGER: An Automata-Based String Analysis Tool for PHP / Fang Yu ; Muath Alkhalaf ; Tevfik Bultan
Automata Theory
When Simulation Meets Antichains: On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata / Parosh Aziz Abdulla ; Yu-Fang Chen ; Lukás Holík ; Richard Mayr ; Tomás Vojnar
On Weak Modal Compatibility, Refinement, and the MIO Workbench / Sebastian S. Bauer ; Philip Mayer ; Andreas Schroeder ; Rolf Hennicker
Rational Synthesis / Dana Fisman ; Orna Kupferman ; Yoad Lustig
Efficient Büchi University Checking / Seth Fogarty ; Moshe Y. Vardi
Liveness
Automated Termination Analysis for Programs with Second-Order Recursion / Markus Aderhold
Ranking Function Synthesis for Bit-Vector Relations / Byron Cook ; Philipp Rümmer ; Christoph M. Wintersteiger
Fairness for Dynamic Control / Jochen Hoenicke ; Ernst-Rüdiger Olderog ; Andreas Podelski
Tools II
JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution / Axel Belinfante
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems / Klaus Dräger ; Andrey Kupriyanov ; Bernd Finkbeiner ; Heike Wehrheim
Tracking Heaps That Hop with Heap-Hop / Jules Villard ; Étienne Lozes ; Cristiano Calcagno
Software Verification
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors / Alastair F. Donaldson
Simplifying Linearizability Proofs with Reduction and Abstraction / Tayfun Elmas ; Shaz Qadeer ; Ali Sezgin ; Omer Subasi ; Serdar Tasiran
A Polymorphic Intermediate Verification Language: Design and Logical Encoding / K. Rustan M. Leino
Trace-Based Symbolic Analysis for Atomicity Violations / Chao Wang ; Rhishikesh Limaye ; Malay Ganai ; Aarti Gupta
Tools III
ACS: Automatic Converter Synthesis for SoC Bus Protocols / Karin Avnit ; Arcot Sowmya ; Jorgen Peddersen
AlPiNA: An Algebraic Petri Net Analyzer / Didier Buchs ; Steve Hostettler ; Alexis Marechal ; Matteo Risoldi
PASS: Abstraction Refinement for Infinite Probabilistic Models / Ernst Moritz Hahn ; Holger Hermanns ; Björn Wachter
Real Time and Information Flow
Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions / Matthieu Moy ; Karine Altisen
Computing the Leakage of Information-Hiding Systems / Miguel E. Andrés ; Catuscia Palamidessi ; Peter van Rossum ; Geoffrey Smith
Statistical Measurement of Information Leakage / Konstantinos Chatzikokolakis ; Tom Chothia ; Apratim Guha
SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata / Janusz Malinowski ; Peter Niebert
Testing
Preemption Sealing for Efficient Concurrency Testing / Thomas Ball ; Sebastian Burckhardt ; Katherine E. Coons ; Madanlal Musuvathi
Code Mutation in Verification and Automatic Code Correction / Gal Katz ; Doron Peled
Efficient Detection of Errors in Java Components Using Random Environment and Restarts / Pavel Parizek ; Tomas Kalibera
Author Index
Invited Talks
Embedded Systems Design - Scientific Challenges and Work Directions (Abstract) / Joseph Sifakis
Antichain Algorithms for Finite Automata / Laurent Doyen ; Jean-François Raskin
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼