![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
30th CAV 2018: Oxford, UK
- Hana Chockler, Georg Weissenbacher
:
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II. Lecture Notes in Computer Science 10982, Springer 2018, ISBN 978-3-319-96141-5
Tools
- Hannah Arndt, Christina Jansen, Joost-Pieter Katoen
, Christoph Matheja
, Thomas Noll
:
Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs. 3-11 - Mostafa Hassan, Caterina Urban, Marco Eilers
, Peter Müller
:
MaxSMT-Based Type Inference for Python 3. 12-19 - Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani:
The JKind Model Checker. 20-27 - Vincent Cheval, Steve Kremer, Itsaka Rakotonirina:
The DEEPSEC Prover. 28-36 - Jianwen Li, Rohit Dureja
, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi:
SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability. 37-44 - Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, Vijay Ganesh
:
StringFuzz: A Fuzzer for String Solvers. 45-51
Static Analysis
- Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller
:
Permission Inference for Array Programs. 55-74 - Patrick Cousot
, Roberto Giacobazzi
, Francesco Ranzato
:
Program Analysis Is Harder Than Verification: A Computability Perspective. 75-95
Theory and Security
- Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi:
Automata vs Linear-Programming Discounted-Sum Inclusion. 99-116 - Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan:
Model Checking Indistinguishability of Randomized Security Protocols. 117-135 - Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik:
Lazy Self-composition for Security Verification. 136-156 - Jun Zhang, Pengfei Gao, Fu Song, Chao Wang:
SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. 157-177 - Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee, Viktor Toman
:
Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives. 178-197 - Tom van Dijk:
Attracting Tangles to Solve Parity Games. 198-215
SAT, SMT and Decision Procedures
- Soonho Kong, Armando Solar-Lezama, Sicun Gao:
Delta-Decision Procedures for Exists-Forall Problems over the Reals. 219-235 - Aina Niemetz
, Mathias Preiner
, Andrew Reynolds
, Clark W. Barrett
, Cesare Tinelli
:
Solving Quantified Bit-Vectors Using Invertibility Conditions. 236-255 - Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia:
Understanding and Extending Incremental Determinization for 2QBF. 256-274 - Robert Robere, Antonina Kolokolova, Vijay Ganesh
:
The Proof Complexity of SMT Solvers. 275-293 - Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet:
Model Generation for Quantified Formulas: A Taint-Based Approach. 294-313
Concurrency
- Xinhao Yuan, Junfeng Yang, Ronghui Gu:
Partial Order Aware Concurrency Sampling. 317-335 - Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran:
Reasoning About TSO Programs Using Reduction and Abstraction. 336-353 - Huyen T. T. Nguyen
, César Rodríguez, Marcelo Sousa, Camille Coti
, Laure Petrucci
:
Quasi-Optimal Partial Order Reduction. 354-371 - Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer:
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. 372-391 - Elvira Albert
, Miguel Gómez-Zamalloa
, Miguel Isabel
, Albert Rubio
:
Constrained Dynamic Partial Order Reduction. 392-410
CPS, Hardware, Industrial Applications
- Mark Tullsen, Lee Pike, Nathan Collins, Aaron Tomb:
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. 413-429 - Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, Eddy Westbrook:
Continuous Formal Verification of Amazon s2n. 430-446 - Daniel Schemmel
, Julian Büning
, Oscar Soria Dustmann, Thomas Noll
, Klaus Wehrle
:
Symbolic Liveness Analysis of Real-World Software. 447-466 - Byron Cook, Kareem Khazem, Daniel Kroening
, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle:
Model Checking Boot Code from AWS Data Centers. 467-486 - Taolue Chen
, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan:
Android Stack Machine. 487-504 - Christoph Walther
:
Formally Verified Montgomery Multiplication. 505-522 - Eric Goubault, Sylvie Putot, Lorenz Sahlmann:
Inner and Outer Approximating Flowpipes for Delay Differential Equations. 523-541
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.