| 10:15–10:16 |
Thomas Pani, Georg Weissenbacher and Florian Zuleger |
Rely-Guarantee Reasoning for Automated Bound Analysis of Concurrent, Shared-Memory Program |
Poster / Slides |
| 10:17–10:18 |
Bjørnar Luteberget |
On synthesis and optimization of railway signalling and interlocking designs |
Poster / Slides |
| 10:19–10:20 |
David Narváez |
A Formally Verified Symmetry Breaking Tool for SAT |
Poster / Slides |
| 10:21–10:22 |
Yi Chou |
Run-time Assurance for Unmanned Aerial Vehicles using Stochastic Modeling and Reachability Analysis |
Poster / Slides |
| 10:23–10:24 |
Souradeep Dutta |
Verification of Deep Neural Networks |
Poster / Slides |
| 10:25–10:26 |
Makai Mann and Clark Barrett |
Finding Critical Clauses in SMT-based Hardware Verification |
Poster / Slides |
| 10:27–10:28 |
Hari Govind Vediramana Krishnan |
Prioritizing Lemmas While Pushing |
Poster / Slides |
| 10:29–10:30 |
Li Huang and Eun-Young Kan |
SMT-based Probabilistic Analysis of Timing Constraints in Cyber-Physical Systems |
Poster / Slides |
| 10:31–10:32 |
Nikita Zyuzin, Heiko Becker, Eva Darulova and Magnus Myreen |
Formalisation of Affine Arithmetic in Coq |
Poster / Slides |
| 10:33–10:34 |
Jakub Kuderski, Arie Gurfinkel and Jorge Navas |
Type-aware DSA-Style Points-To Analysis for Low Level Code |
Poster / Slides |
| 10:35–10:36 |
Pavel Čadek |
Upper and Lower Loop Bound Estimation by Symbolic Execution and Loop Acceleration |
Poster / Slides |
| 10:37–10:38 |
Anton Xue, Ross Mawhorter, Gian Pietro Farina and Stephen Chong |
Towards the Formalization and Analysis of R |
Poster / Slides |
| 10:39–10:40 |
Maxwell Shinn, Clarence Lehman and Ruzica Piskac |
Runtime verification of scientific software |
Poster / Slides |
| 10:41–10:42 |
Adrian Rebola Pardo |
A Theory of Satisfiability-Preserving Proofs in SAT Solving |
Poster / Slides |
