E-book
Tools and Algorithms for the Construction and Analysis of Systems [electronic resource] : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings / edited by Nir Piterman, Scott A. Smolka.
Record details
- ISBN: 9783642367427
- Physical Description: XXIV, 646 p. 137 illus. online resource.
- Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : 2013.
Search for related items by subject
Search for related items by series
Electronic resources
| On-the-Fly Exact Computation of Bisimilarity Distances | ||
| The Quest for Minimal Quotients for Probabilistic Automata | ||
| LTL Model Checking of Interval Markov Chains | ||
| Ramsey vs. Lexicographic Termination Proving | ||
| Structural Counter Abstraction | ||
| Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors | ||
| The MathSAT5 SMT Solver | ||
| Formula Preprocessing in MUS Extraction | ||
| Proof Tree Preserving Interpolation | ||
| Asynchronous Multi-core Incremental SAT Solving | ||
| Model-Checking Iterated Games | ||
| PRISM-games: A Model Checker for Stochastic Multi-Player Games | ||
| PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus | ||
| An Overview of the mCRL2 Toolset and Its Recent Advances | ||
| Analysis of Boolean Programs | ||
| Weighted Pushdown Systems with Indexed Weight Domains | ||
| Underapproximation of Procedure Summaries for Integer Programs | ||
| Runtime Verification Based on Register Automata | ||
| ^ | ||
| Unbounded Model-Checking with Interpolation for Regular Language Constraints | ||
| eVolCheck: Incremental Upgrade Checker for C | ||
| Intertwined Forward-Backward Reachability Analysis Using Interpolants | ||
| An Integrated Specification and Verification Technique or Highly Concurrent Data Structures | ||
| A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems | ||
| Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory | ||
| Synthesis of Circular Compositional Program Proofs via Abduction | ||
| As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty | ||
| Integer Parameter Synthesis for Timed Automata | ||
| LTL Model-Checking for Malware Detection | ||
| Policy Analysis for Self-administrated Role-Based Access Control | ||
| Model Checking Agent Knowledge in Dynamic Access Control Policies | ||
| Frontiers (Graphics and Quantum) Automatic Testing of Real-Time Graphics Systems | ||
| Equivalence Checking of Quantum Protocols | ||
| ^ | ||
| ^^ | ||
| Encoding Monomorphic and Polymorphic Types | ||
| Deriving Probability Density Functions from Probabilistic Functional Programs | ||
| Tool Demonstrations Polyglot: Systematic Analysis for Multiple Statechart Formalisms | ||
| Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO | ||
| BULL: A Library for Learning Algorithms of Boolean Functions | ||
| AppGuard â Enforcing User Requirements on Android Apps | ||
| Model Checking Database Applications | ||
| Efficient Property Preservation Checking of Model Refinements | ||
| Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking | ||
| Competition on Software Verification Second Competition on Software Verification (Summary of SV-COMP 2013) | ||
| CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution) | ||
| CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution) | ||
| ^ | ||
| ^^ | ||
| CSeq: A Sequentialization Tool for C (Competition Contribution) | ||
| Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution) | ||
| LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution) | ||
| Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution) | ||
| Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution) | ||
| Threader: A Verifier for Multi-threaded Programs (Competition Contribution) | ||
| UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution) | ||
| Ultimate Automizer with SMTInterpol (Competition Contribution). | ||
| ^^ |
