Tools and Algorithms for the Construction and Analysis of Systems
portes grátis
Tools and Algorithms for the Construction and Analysis of Systems
30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I
Finkbeiner, Bernd; Kovacs, Laura
Springer International Publishing AG
04/2024
394
Mole
9783031572456
15 a 20 dias
Descrição não disponível.
SAT and SMT Solving.- DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories.- Z3-Noodler: An Automata-based String Solver.- TaSSAT: Transfer and Share SAT.- Speculative SAT modulo SAT.- Happy Ending: An Empty Hexagon in Every Set of 30 Points.- Synthesis.- Fully Generalized Reactivity(1) Synthesis.- Knor: reactive synthesis using Oink.- On Dependent Variables in Reactive Synthesis.- CESAR: Control Envelope Synthesis via Angelic Refinements.- Logic and Decidability.- Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains.- Deciding Boolean Separation Logic via Small Models.- Asynchronous Subtyping by Trace Relaxation.- Program Analysis and Proofs.- SootUp: A Redesign of the Soot Static Analysis Framework.- Formally verified asymptotic consensus in robust networks.- Formally Verifying an Efficient Sorter.- Explainable Online Monitoring of Metric First-Order Temporal Logic.- Proof Checking.- IsaRare: Automatic Veri cation of SMT Rewrites in Isabelle/HOL.- Automate where Automation Fails: Proof Strategies for Frama-C/WP.- VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification.- A Logical Treatment of Finite Automata.- A State-of-the-Art Karp-Miller Algorithm Certified in Coq.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
TACAS;formal verification;software systems;hardware systems;static analysis;probabilistic programming;Open Access;program synthesis;concurrency;testing;simulations;verification of machine
SAT and SMT Solving.- DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories.- Z3-Noodler: An Automata-based String Solver.- TaSSAT: Transfer and Share SAT.- Speculative SAT modulo SAT.- Happy Ending: An Empty Hexagon in Every Set of 30 Points.- Synthesis.- Fully Generalized Reactivity(1) Synthesis.- Knor: reactive synthesis using Oink.- On Dependent Variables in Reactive Synthesis.- CESAR: Control Envelope Synthesis via Angelic Refinements.- Logic and Decidability.- Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains.- Deciding Boolean Separation Logic via Small Models.- Asynchronous Subtyping by Trace Relaxation.- Program Analysis and Proofs.- SootUp: A Redesign of the Soot Static Analysis Framework.- Formally verified asymptotic consensus in robust networks.- Formally Verifying an Efficient Sorter.- Explainable Online Monitoring of Metric First-Order Temporal Logic.- Proof Checking.- IsaRare: Automatic Veri cation of SMT Rewrites in Isabelle/HOL.- Automate where Automation Fails: Proof Strategies for Frama-C/WP.- VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification.- A Logical Treatment of Finite Automata.- A State-of-the-Art Karp-Miller Algorithm Certified in Coq.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
