ATVA 2018: INTERNATIONAL SYMPOSIUM ON AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS
PROGRAM

Days: Sunday, October 7th Monday, October 8th Tuesday, October 9th Wednesday, October 10th

Sunday, October 7th

View this program: with abstractssession overviewtalk overview

10:00-10:30Coffee Break
10:30-11:30 Session 3: Tutorial 1-B
10:30
Recent advances in SMT (cont'd) (abstract)
11:30-12:30 Session 4: Tutorial 2-A
11:30
Symbolic Execution and Probabilistic Reasoning (abstract)
12:30-14:00Lunch Break
14:00-15:00 Session 5: Tutorial 2-B
14:00
Symbolic Execution and Probabilistic Reasoning (cont'd) (abstract)
15:00-16:00 Session 6: Tutorial 3-A
15:00
Formal Methods, Machine Learning, and Cyber-Physical Systems (abstract)
16:00-16:30Coffee Break
16:30-17:30 Session 7: Tutorial 3-B
16:30
Formal Methods, Machine Learning, and Cyber-Physical Systems (contd) (abstract)
Monday, October 8th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 10: Invited talk 1
09:00
Towards Verified Artificial Intelligence (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 11: Cyber-physical systems
10:30
A Formally Verified Motion Planners for Autonomous Vehicles (abstract)
11:00
Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems (abstract)
11:30
Neural State Classification for Hybrid Systems (abstract)
12:00-13:30Lunch Break
13:30-15:00 Session 12: Synthesis 1
13:30
What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction (abstract)
14:00
A Symbolic Algorithm for Lazy Synthesis of Eager Strategies (abstract)
14:30
Round-Bounded Control of Parameterized Systems (abstract)
15:00-15:30Coffee Break
15:30-17:30 Session 13: Temporal logics
15:30
Optimal Proofs for Linear Temporal Logic on Lasso Words (abstract)
16:00
A Fragment of Linear Temporal Logic for Universal Very Weak Automata (abstract)
16:30
EVE: A Tool for Temporal Equilibrium Analysis (abstract)
16:45
MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment (abstract)
17:00
Signal Convolution Logic (abstract)
Tuesday, October 9th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 15: Invited talk
09:00
DeepSafe: A Data-driven Approach for Assessing Robustness of Neural Networks (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 16: Stochastic systems 1
10:30
Bisimilarity Distances for Approximate Differential Privacy (abstract)
11:00
Synthesis in pMDPs: A Tale of 1001 Parameters (abstract)
11:30
PSense: Automatic Sensitivity Analysis for Probabilistic Programs (abstract)
12:00-13:30Lunch Break
13:30-15:00 Session 17: Synthesis 2
13:30
Bounded Synthesis of Reactive Programs (abstract)
14:00
Reactive Synthesis of Register Transducers (abstract)
14:30
Maximum Realizability for Linear Temporal Logic Specifications (abstract)
15:00-15:30Coffee Break
15:30-17:30 Session 18: Static analysis and security
15:30
Quantifiers on Demand (abstract)
16:00
Information Leakage in Arbiter Protocols (abstract)
16:30
Robustness Testing of Intermediate Verifiers (abstract)
17:00
Verifying Rust Programs with SMACK (abstract)
17:15
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode (abstract)
Wednesday, October 10th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 19: Invited talk 3
09:00
Z3 to the power of Azure and Azure to the power of Z3 (abstract)
10:00-10:30Coffee Break
10:30-12:00 Session 20: Symbolic methods
10:30
Simulation Algorithms for Symbolic Automata (abstract)
11:00
Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces (abstract)
11:30
Ranking and Repulsing Supermartingales for Approximating Reachability (abstract)
12:00-13:30Lunch Break
13:30-15:00 Session 21: Decision procedures and verification
13:30
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility (abstract)
14:00
Recursive Online Enumeration of All Minimal Unsatisfiable Subsets (abstract)
14:30
Modular Verification of Concurrent Programs via Sequential Model Checking (abstract)
15:00-15:30Coffee Break
15:30-17:30 Session 22: Stochastic systems 2
15:30
Continuous-Time Markov Decisions based on Partial Exploration (abstract)
16:00
Temporal Logic Verification of Stochastic Systems Using Barrier Certificates (abstract)
16:30
Owl: A Library for \omega-Words, Automata, and LTL (abstract)
16:45
Accelerated Model Checking of Parametric Markov Chains (abstract)
17:15
SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems (abstract)