Tools and Algorithms for the Construction and Analysis of Systems

22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings

AvMarsha Chechik,Jean-François Raskin

Häftad, Engelska, 2016

Del i serien Lecture Notes in Computer Science

559 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

This bookconstitutes the proceedings of the 22nd International Conference on Tools andAlgorithms for the Construction and Analysis of Systems, TACAS 2016, which tookplace in Eindhoven, The Netherlands, in April 2016, held as Part of theEuropean Joint Conferences on Theory and Practice of Software, ETAPS 2016.The 44 full papers presented in this volume were carefully reviewed and selectedfrom 175 submissions. They were organized in topical sections named: abstractionand verification; probabilistic and stochastic systems; synthesis; tool papers;concurrency; tool demos; languages and automata; security; optimization; andcompetition on software verification – SV-COMP.

Produktinformation

Utgivningsdatum:2016-04-09
Mått:155 x 235 x 53 mm
Vikt:1 457 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:961
Upplaga:16001
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783662496732

Utforska kategorier

Systemvetenskap och AI inom Data och IT
Programmeringsböcker inom Data och IT

Innehållsförteckning

Robots at the Edge of the Cloud.- FindingRecurrent Sets with Backward Analysis and Trace Partitioning.- Tactics for theDafny Program Verifier.- Synthesizing Ranking Functions from Bits and Pieces.- AbstractionRefinement and Antichains for Trace Inclusion of Infinite State Systems.- Probabilisticand Stochastic Systems Efficient Syntax-driven Lumping of DifferentialEquations.- Faster Statistical Model Checking for Unbounded TemporalProperties.- Safety-constrained Reinforcement Learning for MDPs.- Safety Verificationof Continuous-Space Pure Jump Markov Processes.- Abstract Learning Frameworksfor Synthesis.- Synthesizing Piece-wise Functions by Learning Classifiers.- AnAutomaton Learning Approach to Solving Safety Games over Infinite Graphs.-Uncertainty Propagation using Probabilistic Affine Forms and Concentration ofMeasure Inequalities.- Online and Compositional Learning of Controllers withApplication to Floor Heating.- Deductive Proofs of Almost Sure Persistence andRecurrence Properties.- Probabilistic CTL* : The Deductive Way.- ParametricRuntime Verification of C Programs.- Coqoon: an IDE for interactive proofdevelopment in Coq.- Multi-core symbolic bisimulation minimization.- Advancesin Symbolic Probabilistic Model Checking with PRISM.- PRISM-PSY: PreciseGPU-Accelerated Parameter Synthesis for Stochastic Systems.- T2: Temporal PropertyVerification.- RTD-Finder: A Tool for Compositional Verification of Real-Time Component-basedSystems.- TcT: Tyrolean Complexity Tool.- Integrated Environment for DiagnosingVerification Errors.- JDart: A Dynamic Symbolic Analysis Framework.- DiagnosticInformation for Control-Flow Analysis of Workflow Graphs.- Approaching theCoverability Problem Continuously.- On Atomicity in Presence of Non-atomicWrites.- Formalizing and Checking Thread Refinement for Data-Race-Free ExecutionModels.- The xSAP Safety Analysis Platform.- FACT: A Probabilistic ModelChecker for Formal Verification with Confidence Intervals.- PrDK: ProtocolProgramming with Automata.- DLC: Compiling a Concurrent System Formal Specificationto a Distributed Implementation.- PRISM-games 2.0: A Tool for Multi-ObjectiveStrategy Synthesis for Stochastic Games.- Cerberus: Automated Synthesis ofEnforcement Mechanisms for Security-sensitive Business Processes.- Developing& Debugging Proof Strategies by Tinkering.- v2c - A Verilog to C TranslatorTool.- Parameterized Compositional Model Checking.- An O(m log n) Algorithm forStuttering Equivalence and Branching Bisimulation.- Interpolants in NonlinearTheories over the Reals.- PTIME Computation of Transitive Closures of OctagonalRelations.- Verification of Linear Controller Software.- Partial OrderReduction for Event-driven Multi-threaded Programs.- Acceleration in Multi-PushdownSystems.- Reduction of Nondeterministic Tree Automata.- Online Timed PatternMatching using Derivatives.- Hybridization based CEGAR for Hybrid Automata withAffine Dynamics.- Complementing Semi-deterministic Buechi Automata.- ReasoningAbout Information Flow Security of Separation Kernels with Channel-basedCommunication.- Some Complexity Results for Stateful Network Verification.- CharacteristicFormulae for Session Types.- Bit-Vector Optimization.- Runtime Monitoring withUnion-Find Structures.- Competition on Software Verification: SV-COMP.- Reliable and Reproducible Competition Results withBenchExec and Witnesses (Report on SV-COMP 2016).