>> Google Books

Tools and Algorithms for the Construction and Analysis of Systems : 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings

フォーマット:
電子ブック
責任表示:
edited by Christel Baier, Cesare Tinelli
言語:
英語
出版情報:
Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2015
形態:
XVIII, 725 p. 210 illus
著者名:
シリーズ名:
Lecture Notes in Computer Science ; 9035
目次情報:
Scalable Timing Analysis with Refinement
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
Verified Reachability Analysis of Continuous Systems
HyComp: An SMT-Based Model Checker for Hybrid Systems
C2E2: A Verification Tool for Stateflow Models
Non-cumulative Resource Analysis
Value Slice: A New Slicing Concept for Scalable Property Checking
A Method for Improving the Precision and Coverage of Atomicity Violation Predictions
Commutativity of Reducers
Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling
Analysis of Dynamic Process Networks
MULTIGAIN: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives
syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
vZ - An Optimizing SMT Solver
dReach: δ-Reachability Analysis for Hybrid Systems
Uppaal Stratego
BINSEC: Binary Code Analysis with Low-Level Regions
Insight: An Open Binary Analysis Framework
SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
Symbolic Model-Checking Using ITS-Tools
Semantic Importance Sampling for Statistical Model Checking
Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
FAUST2: Formal Abstractions of Uncountable-State Stochastic Processes
Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving
On Parallel Scalable Uniform SAT Witness Generation
Approximate Counting in SMT and Value Estimation for Probabilistic Programs
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
Stateless Model Checking for TSO and PSO
GPU Accelerated Strong and Branching Bisimilarity Checking
Fairness for Infinite-State Systems
Software Verification and Verifiable Witnesses
AProVE: Termination and Memory Safety of C Programs
Cascade
CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation
Framework for Embedded System Verification
Forester: Shape Analysis Using Tree Automata
MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings
Perentie: Modular Trace Refinement and Selective Value Tracking
Predator Hunting Party
SeaHorn: A Framework for Verifying C Programs
SMACK+Corral: A Modular Verifier
Ultimate Automizer with Array Interpolation
Ultimate Kojak with Memory Safety Checks
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches
FuncTion: An Abstract Domain Functor for Termination
Model Checking Gene Regulatory Networks
Symbolic Quantitative Robustness Analysis of Timed Automata
Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
Shield Synthesis: Runtime Enforcement for Reactive Systems
Verifying Concurrent Programs by Memory Unwinding
AutoProof: Auto-Active Functional Verification of Object-Oriented Programs
An LTL Proof System for Runtime Verification
MARQ: Monitoring at Runtime with QEA
Parallel Explicit Model Checking for Generalized Bchi Automata
Limit Deterministic and Probabilistic Automata for LTL\GU
Saturation-Based Incremental LTL Model Checking with Inductive Proofs
Nested Antichains for WS1S
Sylvan: Multi-core Decision Diagrams
LTSmin: High-Performance Language-Independent Model Checking
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
Scalable Timing Analysis with Refinement
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
Verified Reachability Analysis of Continuous Systems
HyComp: An SMT-Based Model Checker for Hybrid Systems
C2E2: A Verification Tool for Stateflow Models
Non-cumulative Resource Analysis
続きを見る
書誌ID:
LB00386684
ISBN:
9783662466803 [3662466805]  CiNii Books  Webcat Plus  Google Books
9783662466810 [3662466813]  CiNii Books  Webcat Plus  Google Books
子書誌情報
Loading
オンライン
所蔵情報
Loading availability information

類似資料:

1
 
2
 
3
 
4
 
5
 
6
 
7
 
8
 
9
 
10
 
11
 
12
 

Pitts, Andrew, SpringerLink (Online service)

Springer Berlin Heidelberg : Imprint: Springer

Piterman, Nir, SpringerLink (Online service)

Springer International Publishing : Imprint: Springer

Egyed, Alexander, Schaefer, Ina, SpringerLink (Online service)

Springer Berlin Heidelberg : Imprint: Springer

D’Souza, Deepak, Lal, Akash, Larsen, Kim Guldstrand, SpringerLink (Online service)

Springer Berlin Heidelberg : Imprint: Springer

Franke, Bjorn, SpringerLink (Online service)

Springer Berlin Heidelberg : Imprint: Springer

Blanchette, Jasmin Christian, Kosmatov, Nikolai, SpringerLink (Online service)

Springer International Publishing : Imprint: Springer

Calinescu, Radu, Rumpe, Bernhard, SpringerLink (Online service)

Springer International Publishing : Imprint: Springer

Bartocci, Ezio, Majumdar, Rupak, SpringerLink (Online service)

Springer International Publishing : Imprint: Springer

Focardi, Riccardo, Myers, Andrew, SpringerLink (Online service)

Springer Berlin Heidelberg : Imprint: Springer

Graf, Susanne, Viswanathan, Mahesh, SpringerLink (Online service)

Springer International Publishing : Imprint: Springer

Vitek, Jan, SpringerLink (Online service)

Springer Berlin Heidelberg : Imprint: Springer

Parisi-Presicce, Francesco, Westfechtel, Bernhard, SpringerLink (Online service)

Springer International Publishing : Imprint: Springer