Tools and Algorithms for the Construction and Analysis of Systems : 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS - neues Buch

EAN (ISBN-13): 9783642548628
Erscheinungsjahr: 2014
Herausgeber: Springer Berlin Heidelberg

Buch in der Datenbank seit 2016-07-17T00:15:35+02:00 (Berlin)
Detailseite zuletzt geändert am 2023-03-07T00:01:19+01:00 (Berlin)
ISBN/EAN: 9783642548628

ISBN - alternative Schreibweisen:
978-3-642-54862-8
Alternative Schreibweisen und verwandte Suchbegriffe:
Titel des Buches: algorithms, software tools, theory construction

---

Daten vom Verlag:

Autor/in: Erika Abraham; Klaus Havelund
Titel: Theoretical Computer Science and General Issues; Lecture Notes in Computer Science; Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings
Verlag: Springer; Springer Berlin
652 Seiten
Erscheinungsjahr: 2014-03-21
Berlin; Heidelberg; DE
Sprache: Englisch
53,49 € (DE)
55,00 € (AT)
59,00 CHF (CH)
Available
XVIII, 652 p. 142 illus.

EA; E107; eBook; Nonbooks, PBS / Informatik, EDV/Informatik; Theoretische Informatik; Verstehen; algorithms; automata theory; complexity; decision procedures; dynamic analysis; formal methods; hardware verification; hybrid models; logic; model checking; models of computation; probabilistic systems; program specifications; programming languages; realtime; software engineering; softwrae verification; static analysis; theorem proving; timed models; C; Computer Science Logic and Foundations of Programming; Algorithms; Software Engineering; Theory of Computation; Compilers and Interpreters; Formal Languages and Automata Theory; Computer Science; Algorithmen und Datenstrukturen; Software Engineering; Compiler und Übersetzer; BC

Variations on Safety.- Decision Procedures and their Application in Analysis Decision Procedures for Flat Array Properties.- SATMC: A SAT-Based Model Checker for Security-Critical Systems.- IC3 Modulo Theories via Implicit Predicate Abstraction.- SMT-Based Verification of Software Countermeasures against Side-Channel Attacks.- Detecting Unrealizable Specifications of Distributed Systems.- Synthesizing Safe Bit-Precise Invariants.- PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence.- GRASShopper: Complete Heap Verification with Mixed Specifications.- Alternating Runtime and Size Complexity Analysis of Integer Programs.- Proving Non termination via Safety.- Ranking Templates for Linear Loops.- Modeling and Model Checking Discrete Systems FDR3 — A Modern Refinement Checker for CSP.- Concurrent Depth-First Search Algorithms.- Basic Problems in Multi-View Modeling.- GPU explore: Many-Core On-the-Fly State Space Exploration Using GPUs.- Forward Reachability Computation for Autonomous Max-Plus-Linear Systems.- Compositional Invariant Generation for Timed Systems.- Characterizing Algebraic Invariants by Differential Radical Invariants.- Quasi-Equal Clock Reduction: More Networks, More Queries.- Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata.- Monitoring, Fault Detection and Identification Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic.- Monitoring Modulo Theories.- Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems.- Status Report on Software Verification (Competition Summary SV-COMP 2014).- CBMC – C Bounded Model Checker (Competition Contribution).- CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution).- CPALIEN: Shape Analyzer for CPAChecker (Competition Contribution).- Lazy-CSeq: A Lazy Sequentialization Tool for C (CompetitionContribution).- MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution).- ESBMC 1.22 (Competition Contribution).- FrankenBit: Bit-Precise Verification with Many Bits (Competition Contribution).- Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution).- Symbiotic 2: More Precise Slicing (Competition Contribution).- Ultimate Automizer with Unsatisfiable Cores (Competition Contribution).- Ultimate Kojak (Competition Contribution).- Specifying and Checking Linear Time Properties Discounting in LTL.- Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata.- Symbolic Synthesis for Epistemic Specifications with Observational Semantics.- Synthesis for Human-in-the-Loop Control Systems.- Learning Regular Languages over Large Alphabets.- Verification of Concurrent Quantum Protocols by Equivalence Checking.- Computing Conditional Probabilities in Markovian Models Efficiently.- Permissive Controller Synthesis for Probabilistic Systems.- Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance.- SACO: Static Analyzer for Concurrent Objects.- VeriMAP: A Tool for Verifying Programs through Transformations.- CIF 3: Model-Based Engineering of Supervisory Controllers.- EDD: A Declarative Debugger for Sequential Erlang Programs.- APTE: An Algorithm for Proving Trace Equivalence.- The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification.- Bounds2: A Tool for Compositional Multi-parametrised Verification.- On the Correctness of a Branch Displacement Algorithm.- Analyzing the Next Generation Airborne Collision Avoidance System.- Environment-Model Based Testing of Control Systems: Case Studies.