Search Results - "Smt."
Suggested Topics within your search.
Suggested Topics within your search.
- Software Engineering 35
- Computer science 27
- Artificial intelligence 24
- Software engineering 19
- Computer programming / software development 16
- Mathematical theory of computation 16
- Algorithms & data structures 12
- Artificial Intelligence 10
- Computer Science Logic and Foundations of Programming 10
- Theory of Computation 10
- Computer Engineering and Networks 8
- Computer engineering 8
- Computer networks 8
- Formal Languages and Automata Theory 8
- Machine theory 8
- Systems analysis & design 8
- Computer Modelling 7
- Computer simulation 7
- Control Structures and Microprogramming 7
- Microprogramming 7
- Computer networking & communications 6
- Computers 6
- Electronic digital computers 5
- Evaluation 5
- System Performance and Evaluation 5
- Computer modelling & simulation 4
- Expert systems / knowledge-based systems 4
- Professions 4
- The Computing Profession 4
- Algorithms 3
-
61
-
62
-
63
-
64
-
65
-
66
-
67
-
68
-
69
Tools and Algorithms for the Construction and Analysis of Systems 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice o...
Published 2019Table of Contents: “…SAT and SMT -- Decomposing Farkas Interpolants -- Parallel SAT Simplification on GPU Architectures -- Encoding Redundancy for Satisfaction-Driven Clause Learning -- WAPS: Weighted and Projected Sampling -- Building Better Bit-Blasting for Floating-Point Problems -- The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations -- On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition -- Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework -- SAT Solving and Theorem Proving -- Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks -- Incremental Analysis of Evolving Alloy Models -- Extending a Brainiac Prover to Lambda-Free Higher-Order Logic -- Verification and Analysis LCV: A Verification Tool for Linear Controller Software -- Semantic Fault Localization and Suspiciousness Ranking -- Computing Coupled Similarity -- Reachability Analysis for Termination and Confluence of Rewriting -- Model Checking -- VoxLogicA: a Spatial Model Checker for Declarative Image Analysis -- On Reachability in Parameterized Phaser Programs -- Abstract Dependency Graphs and Their Application to Model Checking -- Tool Demo -- nonreach - A Tool for Nonreachability Analysis -- The Quantitative Verification Benchmark Set -- ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions -- MetAcsl: Specification and Verification of High-Level Properties -- ROLL 1.0: !…”
Link to Metadata
Electronic eBook -
70
-
71
-
72
-
73
Computer Aided Verification 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II /
Published 2019Table of Contents: “…Logics, Decision Procedures, and Solvers -- Satisfiability Checking for Mission-Time LTL -- High-Level Abstractions for Simplifying Extended String Constraints in SMT -- Alternating Automata Modulo First Order Theories -- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors -- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis -- Incremental Determinization for Quantifier Elimination and Functional Synthesis -- Numerical Programs -- Loop Summarization with Rational Vector Addition Systems -- Invertibility Conditions for Floating-Point Formulas -- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems -- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler -- Sound Approximation of Programs with Elementary Functions -- Verification -- Formal verification of quantum algorithms using quantum Hoare logic -- SecCSL: Security Concurrent Separation Logic -- Reachability Analysis for AWS-based Networks -- Distributed Systems and Networks -- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics -- Gradual Consistency Checking -- Checking Robustness Against Snapshot Isolation -- Efficient verification of network fault tolerance via counterexampleguided refinement -- On the Complexity of Checking Consistency for Replicated Data Types -- Communication-closed asynchronous protocols -- Verification and Invariants -- Interpolating Strong Induction -- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers -- Inferring Inductive Invariants from Phase Structures -- Termination of Triangular Integer Loops is Decidable -- AliveInLean: A Verified LLVM Peephole Optimization Verifier -- Concurrency -- Automated Parameterized Verification of CRDTs -- What's wrong with on-the-y partial order reduction -- Integrating Formal Schedulability Analysis into a Verifed OS Kernel -- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS -- Violat: Generating Tests of Observational Refinement for Concurrent Objects. .…”
Link to Metadata
Electronic eBook -
74
Tools and Algorithms for the Construction and Analysis of Systems 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice o...
Published 2022Table of Contents: “…Synthesis -- HOLL: Program Synthesis for Higher Order Logic Locking -- The Complexity of LTL Rational Synthesis -- Synthesis of Compact Strategies for Coordination Programs -- ZDD Boolean Synthesis -- Verification -- 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 -- Blockchain -- Formal Verification of the Ethereum 2.0 Beacon Chain -- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover -- A Max-SMT Superoptimizer for EVM handling Memory and Storage -- Grammatical Inference -- 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 -- and Daniel NeiderLearning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes -- Verification Inference -- Inferring Interval-Valued Floating-Point Preconditions -- NeuReach: Learning Reachability Functions from Simulations -- Quantifier Alternations: Taming the Search Space Explosion -- LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions -- Short papers -- 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 -- Constraint Solving -- 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 -- Model checking and verification -- Property Directed Reachability for Generalized Petri Nets -- Transition Power Abstractions for Deep Counterexample Detection -- Searching for Ribbon-Shaped Paths in Fair Transition Systems -- CoVeriTeam: On-Demand Composition of Cooperative Verification Systems.…”
Link to Metadata
Electronic eBook -
75
-
76
-
77
-
78
Tools and Algorithms for the Construction and Analysis of Systems 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice o...
Published 2023Table of Contents: “…-A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems -- Model Checking -- Bounded Model Checking for Asynchronous Hyperproperties -- Model Checking Linear Dynamical Systems under Floating-point Rounding -- Efficient Loop Conditions for Bounded Model Checking Hyperproperties -- Reconciling Preemption Bounding with DPOR -- Optimal Stateless Model Checking for Causal Consistency -- Symbolic Model Checking for TLA+ Made Faster -- AutoHyper: Explicit-State Model Checking for HyperLTL -- Machine Learning/Neural Networks -- Feature Necessity & Relevancy in ML Classifier Explanations -- Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks -- OccRob: Effcient SMT-Based Occlusion Robustness Verification of Deep Neural Networks -- Neural Network-Guided Synthesis of Recursive List Functions -- Automata -- Modular Mix-and-Match Complementation of Buechi automata -- Validating Streaming JSON Documents With Learned VPAs -- Antichains Algorithms for the Inclusion Problem Between ω -VPL -- Stack-Aware Hyperproperties -- Proofs -- Propositional Proof Skeletons -- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers -- Carcara: An effcient proof checker and elaborator for SMT proofs in the Alethe format -- Constraint Solving/Blockchain -- The Packing Chromatic Number of the Infinite Square Grid is 15 -- Active Learning for SAT Solver Benchmarking -- ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving -- Inferring Needless Write Memory Accesses on Ethereum Bytecode -- Markov Chains/Stochastic Control -- A Practitioner's Guide to MDP Model Checking Algorithms -- Correct Approximation of Stationary Distributions -- Robust Almost-Sure Reachability in Multi-Environment MDPs -- Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning -- Verification -- A Formal CHERI-C Semantics for Verification -- Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm -- Parameterized Verification under TSO with Data Types -- Verifying Learning-Based Robotic Navigation Systems: A Case Study -- Make flows small again: revisiting the flow framework -- ALASCA: Reasoning in Quantified Linear Arithmetic -- A Matrix-Based Approach to Parity Games -- A GPU Tree Database for Many-Core Explicit State Space Exploration.…”
Link to Metadata
Electronic eBook -
79
Tools and Algorithms for the Construction and Analysis of Systems 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice o...
Published 2022Table of Contents: “…Probabilistic Systems -- A Probabilistic Logic for Verifying Continuous-time Markov Chains -- Under-Approximating Expected Total Rewards in POMDPs -- Correct Probabilistic Model Checking with Floating-Point Arithmetic -- Correlated Equilibria and Fairness in Concurrent Stochastic Games -- Omega Automata -- A Direct Symbolic Algorithm for Solving Stochastic Rabin Games -- Practical Applications of the Alternating Cycle Decomposition -- Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation -- On-The-Fly Solving for Symbolic Parity Games -- Equivalence Checking -- Distributed Coalgebraic Partition Refinement -- From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques -- Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time -- Monitoring and Analysis -- A Theoretical Analysis of Random Regression Test Prioritization -- Verified First-Order Monitoring with Recursive Rules -- Maximizing Branch Coverage withConstrained Horn Clauses -- Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation -- Tools / Optimizations, Repair and Explainability -- Adiar: Binary Decision Diagrams in External Memory -- Forest GUMP: A Tool for Explanation -- Alpinist: an Annotation-Aware GPU Program Optimizer -- Automatic Repair for Network Programs -- 11th Competition on Software Verification / SV-COMP 2022 -- Progress on Software Verification: SV-COMP 2022 -- AProVE: Non-Termination Witnesses for C Programs (Competition Contribution) -- BRICK: Path Enumeration Based Bounded Reachability Checking of C Program (Competition Contribution) -- A Prototype for Data Race Detection in CSeq 3 (Competition Contribution) -- Dartagnan: SMT-based Violation Witness Validation (Competition Contribution) -- Deagle: An SMT-based Veri er for Multi-threaded Programs (Competition Contribution) -- The Static Analyzer Frama-C in SV-COMP (Competition Contribution) -- GDart: An Ensemble of Tools for Dynamic Symbolic Execution on the Java Virtual Machine (Competition Contribution) -- Graves-CPA: A Graph-Attention Veri er Selector (Competition Contribution) -- GWIT: A Witness Validator for Java based on GraalVM (Competition Contribution) -- The Static Analyzer Infer in SV-COMP (Competition Contribution) -- LART: Compiled Abstract Execution (Competition Contribution) -- Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding (Competition Contribution) -- Symbiotic-Witch: A Klee-Based Violation Witness Checker (Competition Contribution) -- Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection -- Ultimate GemCutter and the Axes of Generalization (Competition Contribution) -- Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution).…”
Link to Metadata
Electronic eBook -
80