the proceedings contain 42 papers from the tools and algorithms for the construction and analysis of systems - 11thinternationalconference, TACAS 2005, held as part of the Joint European conferences on theory and Pr...
详细信息
the proceedings contain 42 papers from the tools and algorithms for the construction and analysis of systems - 11thinternationalconference, TACAS 2005, held as part of the Joint European conferences on theory and Practice of Software, ETAPS 2005. the topics discussed include: applications of Craig interpolants in model checking;simulation-based iteration of trees transducers;on-the-fly reachability and cycle detection for recursive state machines;context-bounded model checking of concurrent software;a generic theorem prover of CSP refinement;an abstract interpretation-based refinement algorithm for strong preservation;a note on on-the-fly verification algorithms;and complimentation constructions for nondeterministic automata on infinite words.
tools and algorithms for the construction and analysis of systems : 5thinternationalconference, Tacas '99, Held as Part of the Joint European conferences on theory and Practice of Software, Etaps '99, Amster...
详细信息
tools and algorithms for the construction and analysis of systems : 5thinternationalconference, Tacas '99, Held as Part of the Joint European conferences on theory and Practice of Software, Etaps '99, Amsterdam, the Netherlands, March 22-28, 1999 : Proceedings by Tacas '99 (1999 : Amsterdam, Netherlands); Cleaveland, W. R. (Walter Rance), 1961-; Etaps '99 (1999 : Amsterdam, Netherlands); published by Berlin ; New York : Springer
the proceedings contain 22 papers. the special focus in this conference is on tools and algorithms for the construction and analysis of systemsconference series. the topics include: Shepherding hordes of markov chain...
ISBN:
(纸本)9783030174644
the proceedings contain 22 papers. the special focus in this conference is on tools and algorithms for the construction and analysis of systemsconference series. the topics include: Shepherding hordes of markov chains;optimal time-bounded reachability analysis for concurrent systems;minimal-time synthesis for parametric timed automata;Environmentally-Friendly GR(1) Synthesis;stocHy: Automated Verification and Synthesis of Stochastic Processes;synthesis of symbolic controllers: A parallelized and sparsity-aware approach;iRank: A variable order metric for deds subject to linear invariants;binary decision diagrams with edge-specified reductions;effective entailment checking for separation logic with inductive definitions;Digital Bifurcation analysis of TCP Dynamics;the mCRL2 toolset for Analysing Concurrent systems: Improvements in Expressivity and Usability;verifying safety of synchronous fault-tolerant algorithms by bounded model checking;measuring masking fault-tolerance;PhASAR: An Inter-procedural Static analysis Framework for C/C++;automatic analysis of consistency properties of distributed transaction systems in maude;multi-core On-the-Fly Saturation;Specification and efficient monitoring beyond STL;VyPR2: A framework for runtime verification of python web services;constraint-Based Monitoring of Hyperproperties;tail probabilities for randomized program runtimes via martingales for higher moments;computing the expected execution time of probabilistic workflow nets.
the proceedings contain 36 papers. the topics discussed include: antichain algorithms for finite automata;assume-guarantee verification for probabilistic systems;model checking interactive Markov chains;approximating ...
ISBN:
(纸本)3642120016
the proceedings contain 36 papers. the topics discussed include: antichain algorithms for finite automata;assume-guarantee verification for probabilistic systems;model checking interactive Markov chains;approximating the Pareto front of multi-criteria optimization problems;an alternative to sat-based approaches for bit-vectors;satisfiability modulo the theory of costs: foundations and applications;optimal tableau algorithms for coalgebraic logics;when simulation meets antichains: on checking language inclusion of nondeterministic finite (tree) automata;on weak modal compatibility, refinement, and the MIO workbench;automated termination analysis for programs with second-order recursion;ranking function synthesis for bit-vector relations;fairness for dynamic control;tracking heaps that hop with heap-hop;automatic analysis of scratch-pad memory code for heterogeneous multicore processors;and trace-based symbolic analysis for atomicity violations.
the proceedings contain 54 papers. the topics discussed include: verifying object-oriented software: lessons and challenges;shape analysis by graph decomposition;a reachability predicate for analyzing low-level softwa...
详细信息
the proceedings contain 54 papers. the topics discussed include: verifying object-oriented software: lessons and challenges;shape analysis by graph decomposition;a reachability predicate for analyzing low-level software;generating representation invariants of structurally complex data;multi-objective model checking of Markov decision processes;PReMo: an analyzer for probabilistic recursive models;counterexamples in probabilistic model checking;bisimulation minimisation mostly speeds up probabilistic model checking;causal dataflow analysis for concurrent programs;a symbolic algorithm for optimal Markov chain lumping;flow faster: efficient decision algorithms for probabilistic simulations;model checking probabilistic timed automata with one or two clocks;adaptor synthesis for real-time components;deciding an interval logic with accumulated durations;complexity in simplicity: flexible agent-based state space exploration;and assume-guarantee synthesis.
the proceedings contain 22 papers. the special focus in this conference is on tools and algorithms for the construction and analysis of systemsconference series. the topics include: the 2019 Comparison of tools for t...
ISBN:
(纸本)9783030175016
the proceedings contain 22 papers. the special focus in this conference is on tools and algorithms for the construction and analysis of systemsconference series. the topics include: the 2019 Comparison of tools for the analysis of Quantitative Formal Models: (QComp 2019 Competition Report);the Rewrite Engines Competitions: A RECtrospective;RERS 2019: Combining Synthesis with Real-World Models;SL-COMP: Competition of Solvers for Separation Logic;Automatic Verification of C and Java Programs: SV-COMP 2019;TOOLympics 2019: An Overview of Competitions in Formal Methods;the Termination and Complexity Competition;international Competition on Software Testing (Test-Comp);verifythis – Verification Competition with a Human Factor;CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker: (Competition Contribution);Extending DIVINE with Symbolic Verification Using SMT: (Competition Contribution);ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference: (Competition Contribution);jayHorn: A Java Model Checker: (Competition Contribution);JBMC: Bounded Model Checking for Java Bytecode: (Competition Contribution);Java Pathfinder at SV-COMP 2019 (Competition Contribution);PeSCo: Predicting Sequential Combinations of Verifiers: (Competition Contribution);confluence Competition 2019;pinaka: Symbolic Execution Meets Incremental Solving: (Competition Contribution);Symbolic Pathfinder for SV-COMP: (Competition Contribution);veriFuzz: Program Aware Fuzzing: (Competition Contribution);ETAPS Foreword;TACAS Preface;preface.
the proceedings contain 35 papers. the special focus in this conference is on Invited Contributions, Real-Time and probabilistic systems, Scheduling, Miscellaneous, Software verification, Infinite-State and parametric...
ISBN:
(纸本)3540434194
the proceedings contain 35 papers. the special focus in this conference is on Invited Contributions, Real-Time and probabilistic systems, Scheduling, Miscellaneous, Software verification, Infinite-State and parametric systems and Model Checking: logics and algorithms. the topics include: Software construction and analysistools for future space missions;alloy;improving the verification of timed systems using influence information;digitisation and full abstraction for dense-time model checking;a hybrid approach;schedulability and decidability;validating timing constraints of dependent jobs with variable execution times in distributed real-time systems;an analysis of zero-clairvoyant scheduling;preemptive job-shop scheduling using stopwatch automata;explicit modeling of influences, and of their absence, in distributed systems;a functional semantics of attribute grammars;relative completeness of abstraction refinement for software model checking;towards the automated verification of multithreaded java programs;CLPS-B - A constraint solver for B;formal verification of functional properties of an SCR-style software requirements specification using PVS;beyond parameterized verification;resource-constrained model checking of recursive programs;model checking large-scale and parameterized resource allocation systems;exploring very large state spaces using genetic algorithms;local model-checking of modal mu-calculus on acyclic labeled transition systems and the forspec temporal logic.
the proceedings contain 67 papers. the special focus in this conference is on tools and algorithms for the construction and analysis of systems. the topics include: A New Approach for Active Automata Learning Based on...
ISBN:
(纸本)9783030995232
the proceedings contain 67 papers. the special focus in this conference is on tools and algorithms for the construction and analysis of systems. the topics include: A New Approach for Active Automata Learning Based on Apartness;learning Realtime One-Counter Automata;scalable Anytime algorithms for Learning Fragments of Linear Temporal Logic;learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes;inferring Interval-Valued Floating-Point Preconditions;neuReach: Learning Reachability Functions from Simulations;inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion;linSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions;the Complexity of LTL Rational Synthesis;Kmclib: Automated Inference and Verification of Session Types from OCaml Programs;automated Translation of Natural Language Requirements to Runtime Monitors;maskD: A Tool for Measuring Masking Fault-Tolerance;better Counterexamples for Dafny;cvc5: A Versatile and Industrial-Strength SMT Solver;clausal Proofs for Pseudo-Boolean Reasoning;moving Definition Variables in Quantified Boolean Formulas;a Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic;property Directed Reachability for Generalized Petri Nets;transition Power Abstractions for Deep Counterexample Detection;synthesis of Compact Strategies for Coordination Programs;searching for Ribbon-Shaped Paths in Fair Transition systems;coVeriTeam: On-Demand Composition of Cooperative Verification systems;ZDD Boolean Synthesis;comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra systems;Verifying Fortran Programs with CIVL;NORMA: a tool for the analysis of Relay-based Railway Interlocking systems;efficient Neural Network analysis with Sum-of-Infeasibilities;formal Verification of the Ethereum 2.0 Beacon Chain.
暂无评论