Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Andreas Katis, Andrew Gacek, Michael W. Whalen |
Machine-Checked Proofs for Realizability Checking Algorithms. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Achim D. Brucker, Oto Havle, Yakoub Nemouchi, Burkhart Wolff |
Testing the IPC Protocol for a Real-Time Operating System. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif |
Inside a Verified Flash File System: Transactions and Garbage Collection. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko |
Recursive Games for Compositional Program Synthesis. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich |
How to Avoid Proving the Absence of Integer Overflows. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Felix Dörre, Vladimir Klebanov |
Pseudo-Random Number Generator Verification: A Case Study. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina |
A Proof-Sensitive Approach for Small Propositional Interpolants. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Eric Smith, Alessandro Coglio |
Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Wojciech Mostowski |
Dynamic Frames Based Verification Method for Concurrent Java Programs. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Ali Sezgin, Serdar Tasiran |
Moving Around: Lipton's Reduction for TSO - (Regular Submission). |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Jonas Oberhauser |
A Simpler Reduction Theorem for x86-TSO. |
VSTTE |
2015 |
DBLP DOI BibTeX RDF |
|
1 | David Sanán, Andrew Butterfield, Mike Hinchey |
Separation Kernel Verification: The Xtratum Case Study. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Wei Yang Tan, Rohit Sinha 0001, John L. Manferdelli, Sanjit A. Seshia |
Formal Modeling and Verification of CloudProxy. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Robbert Krebbers |
Separation Algebras for C Verification in Coq. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich |
Formalizing Semantics with an Automatic Program Verifier. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Anindya Banerjee 0001, David A. Naumann |
A Logical Analysis of Framing for Specifications with Pure Method Calls. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Leo Freitas, Cliff B. Jones, Andrius Velykis, Iain Whiteside |
A Model for Capturing and Replaying Proof Strategies. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Sumesh Divakaran, Deepak D'Souza, Nigamanth Sridhar |
Efficient Refinement Checking in VCC. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Alexis Fouilhé, Sylvain Boulmé |
A Certifying Frontend for (Sub)polyhedral Abstract Domains. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Vijayaraghavan Murali, Nishant Sinha 0001, Emina Torlak, Satish Chandra 0001 |
What Gives? A Hybrid Algorithm for Error Trace Explanation. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | René Neumann |
Using Promela in a Fully Verified Executable LTL Model Checker. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Luca Spalazzi, Francesco Spegni |
Parameterized Model-Checking of Timed Systems with Conjunctive Guards. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Dimitra Giannakopoulou, Daniel Kroening (eds.) |
Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Ernie Cohen, Andrey Rybalchenko (eds.) |
Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Martin Clochard |
Automatically Verified Implementation of Data Structures Based on AVL Trees. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Geng Chen, Ernie Cohen, Mikhail Kovalev |
Store Buffer Reduction with MMUs. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Mohana Asha Latha Dubasi, Sudarshan K. Srinivasan, Vidura Wijayasekara |
Timed Refinement for Verification of Real-Time Object Code Programs. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel 0002, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich |
The KeY Platform for Verification and Analysis of Java Programs. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Madiha Jami, Andrew Ireland |
A Verification Condition Visualizer. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Julian Nagele, René Thiemann, Sarah Winkler |
Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
1 | K. Rustan M. Leino, Nadia Polikarpova |
Verified Calculations. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Pamela Zave, Jennifer Rexford |
Compositional Network Mobility. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich |
Preserving User Proofs across Specification Changes. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang 0004, Lei Yuan, Yu Liu |
Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas P. Jensen |
Result Certification of Static Program Analysers with Automated Theorem Provers. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Julian Tschannen, Carlo A. Furia, Martin Nordio, Bertrand Meyer 0001 |
Program Checking with Less Hassle. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Falke 0001, Florian Merz 0001, Carsten Sinz |
Extending the Theory of Arrays: memset, memcpy, and Beyond. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Anthony Narkawicz, César A. Muñoz |
A Formally Verified Generic Branching Algorithm for Global Optimization. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Assalé Adjé, Olivier Bouissou, Jean Goubault-Larrecq, Eric Goubault, Sylvie Putot |
Static Analysis of Programs with Imprecise Probabilistic Inputs. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif |
Verification of a Virtual Filesystem Switch. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Shilpi Goel, Warren A. Hunt Jr. |
Automated Code Proofs on a Formal Model of the X86. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Philipp Rümmer, Hossein Hojjat, Viktor Kuncak |
Classifying and Solving Horn Clauses for Verification. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Tuan-Hung Pham, Michael W. Whalen |
An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Sandrine Blazy, André Maroneze, David Pichardie |
Formal Verification of Loop Bound Estimation for WCET Analysis. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Jost 0001, Alexander J. Summers |
An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Etienne Kneuss, Viktor Kuncak, Philippe Suter |
Effect Analysis for Programs with Callbacks. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Nicolás Rosner, Carlos Gustavo López Pombo, Nazareno Aguirre, Ali Jaoua, Ali Mili 0001, Marcelo F. Frias |
Parallel Bounded Verification of Alloy Models by TranScoping. |
VSTTE |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Christophe Filliâtre |
Verifying Two Lines of C with Why3: An Exercise in Program Verification. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Nadia Polikarpova, Michal Moskal |
Verifying Implementations of Security Protocols by Refinement. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Rupak Majumdar |
The Marriage of Exploration and Deduction. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Falke 0001, Deepak Kapur, Carsten Sinz |
Termination Analysis of Imperative Programs Using Bitvector Arithmetic. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | K. Rustan M. Leino |
Developing Verified Programs with Dafny. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Sabine Schmaltz, Andrey Shadrin |
Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Gregory Kulczycki, Hampton Smith, Heather K. Harton, Murali Sitaraman, William F. Ogden, Joseph E. Hollingsworth |
The Location Linking Concept: A Basis for Verification of Code Using Pointers. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft |
Formalized Verification of Snapshotable Trees: Separation and Sharing. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Cristiano Bertolini, Martin Schäf, Pascal Schweitzer |
Infeasible Code Detection. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang J. Paul |
Cyber War, Formal Verification and Certified Infrastructure. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Amalinda Post, Jochen Hoenicke |
Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Christopher M. Hayden, Stephen Magill, Michael Hicks 0001, Nate Foster, Jeffrey S. Foster |
Specifying and Verifying the Correctness of Dynamic Software Updates. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Ioannis T. Kassios, Peter Müller 0001, Malte Schwerhoff |
Comparing Verification Condition Generation with Symbolic Execution: An Experience Report. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Eyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul |
Verification of TLB Virtualization Implemented in C. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff |
Isabelle/Circus: A Process Specification and Verification Environment. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Florian Merz 0001, Stephan Falke 0001, Carsten Sinz |
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Loren Segal, Patrice Chalin |
A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Paolo Herms, Claude Marché, Benjamin Monate |
A Certified Multi-prover Verification Condition Generator. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Joshi, Peter Müller 0001, Andreas Podelski (eds.) |
Verified Software: Theories, Tools, Experiments - 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Wies, Marco Muñiz, Viktor Kuncak |
Deciding Functional Lists with Sublist Sets. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Martin Brain, Florian Schanda |
A Lightweight Technique for Distributed and Incremental Program Verification. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Milena Vujosevic-Janicic, Viktor Kuncak |
Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Misty D. Davies, Corina S. Pasareanu, Vishwanath Raman |
Symbolic Execution Enhanced System Testing. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Nguyen Van Tang, Daisuke Souma, Goro Hatayama, Hitoshi Ohsaki |
Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Francesco Logozzo |
Our Experience with the CodeContracts Static Checker - (Invited Tutorial). |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Gerwin Klein |
The L4.verified Project - Next Steps. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse |
Abstraction and Refinement for Local Reasoning. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Eyad Alkassar, Mark A. Hillebrand, Wolfgang J. Paul, Elena Petrova |
Automated Verification of a Small Hypervisor. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | K. Rustan M. Leino, Rosemary Monahan |
Dafny Meets the Verification Benchmarks Challenge. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Tom Ridge |
A Rely-Guarantee Proof System for x86-TSO. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G. Russo |
An Approach of Requirements Tracing in Formal Refinement. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Magnus O. Myreen |
Reusable Verification of a Copying Collector. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, Julien Vanegue |
Towards Scalable Modular Checking of User-Defined Properties. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Michael Barnett 0001, K. Rustan M. Leino |
To Goto Where No Statement Has Gone Before. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Eyad Alkassar, Wolfgang J. Paul, Artem Starostin, Alexandra Tsyban |
Pervasive Verification of an OS Microkernel - Inline Assembly, Memory Consumption, Concurrent Devices. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Stan Rosenberg, Anindya Banerjee 0001, David A. Naumann |
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Ali Sezgin, Serdar Tasiran, Shaz Qadeer |
Tressa: Claiming the Future. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Matthew J. Parkinson |
The Next 700 Separation Logics - (Invited Paper). |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer 0001 |
Specifying Reusable Components. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Gary T. Leavens, Peter W. O'Hearn, Sriram K. Rajamani (eds.) |
Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, Edinburgh, UK, August 16-19, 2010. Proceedings |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Eyad Alkassar, Mark A. Hillebrand |
Formal Functional Verification of Device Drivers. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Bertrand Meyer 0001, Jim Woodcock 0001 (eds.) |
Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Xinyu Feng 0001, Zhong Shao, Yu Guo, Yuan Dong |
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Artem Starostin, Alexandra Tsyban |
Verified Process-Context Switch for C-Programmed Kernels. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Anindya Banerjee 0001, Michael Barnett 0001, David A. Naumann |
Boogie Meets Regions: A Verification Experience Report. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Mark Bickford |
Unguessable Atoms: A Logical Foundation for Security. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Madhu Gopinathan, Aditya V. Nori, Sriram K. Rajamani |
Combining Tests and Proofs. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Joey W. Coleman |
Expression Decomposition in a Rely/Guarantee Context. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Moshe Y. Vardi |
From Verification to Synthesis. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Rafal Kolanski, Gerwin Klein |
Mapped Separation Logic. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Greg Dennis, Kuat Yessenov, Daniel Jackson 0001 |
Bounded Verification of Voting Software. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Bruce W. Weide, Murali Sitaraman, Heather K. Harton, Bruce M. Adcock, Paolo Bucci, Derek Bronish, Wayne D. Heym, Jason Kirschenbaum, David Frazier |
Incremental Benchmarks for Software Verification Tools and Techniques. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Natarajan Shankar, Jim Woodcock 0001 (eds.) |
Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|