| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Rajeev Joshi, Peter Müller 0002, 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 | Rupak Majumdar |
The Marriage of Exploration and Deduction. |
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 | Francesco Logozzo |
Our Experience with the CodeContracts Static Checker - (Invited Tutorial). |
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 | Martin Brain, Florian Schanda |
A Lightweight Technique for Distributed and Incremental Program Verification. |
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 | Wolfgang Paul |
Cyber War, Formal Verification and Certified Infrastructure. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Falke, Deepak Kapur, Carsten Sinz |
Termination Analysis of Imperative Programs Using Bitvector Arithmetic. |
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 | Paolo Herms, Claude Marché, Benjamin Monate |
A Certified Multi-prover Verification Condition Generator. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Christopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster, Jeffrey S. Foster |
Specifying and Verifying the Correctness of Dynamic Software Updates. |
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 | K. Rustan M. Leino |
Developing Verified Programs with Dafny. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Ioannis T. Kassios, Peter Müller, Malte Schwerhoff |
Comparing Verification Condition Generation with Symbolic Execution: An Experience Report. |
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 | Amalinda Post, Jochen Hoenicke |
Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Cristiano Bertolini, Martin Schäf, Pascal Schweitzer |
Infeasible Code Detection. |
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 | Florian Merz, Stephan Falke, Carsten Sinz |
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. |
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 | 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 | Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff |
Isabelle/Circus: A Process Specification and Verification Environment. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Misty Davies, Corina S. Pasareanu, Vishwanath Raman |
Symbolic Execution Enhanced System Testing. |
VSTTE |
2012 |
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 | Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer |
Specifying Reusable Components. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Barnett, K. Rustan M. Leino |
To Goto Where No Statement Has Gone Before. |
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 | Gerwin Klein |
The L4.verified Project - Next Steps. |
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 | Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G. Russo |
An Approach of Requirements Tracing in Formal Refinement. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Stan Rosenberg, Anindya Banerjee, David A. Naumann |
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. |
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 | Tom Ridge |
A Rely-Guarantee Proof System for x86-TSO. |
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 | Magnus O. Myreen |
Reusable Verification of a Copying Collector. |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew J. Parkinson |
The Next 700 Separation Logics - (Invited Paper). |
VSTTE |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ali Sezgin, Serdar Tasiran, Shaz Qadeer |
Tressa: Claiming the Future. |
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 | Moshe Y. Vardi |
From Verification to Synthesis. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Bertrand Meyer, Jim Woodcock (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 | Daniel Leivant |
Propositional Dynamic Logic for Recursive Procedures. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
?-Calculus, fixpoints, recursive procedures, Propositional dynamic logic |
| 1 | Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong |
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Podelski |
Verification, Least-Fixpoint Checking, Abstraction. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Bickford |
Unguessable Atoms: A Logical Foundation for Security. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, Koichi Takahashi |
Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone |
Verified Protection Model of the seL4 Microkernel. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Anindya Banerjee, Michael Barnett, David A. Naumann |
Boogie Meets Regions: A Verification Experience Report. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, Burkhart Wolff |
A Verification Approach for System-Level Concurrent Programs. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Greg Dennis, Kuat Yessenov, Daniel Jackson |
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 | Artem Starostin, Alexandra Tsyban |
Verified Process-Context Switch for C-Programmed Kernels. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrice Chalin, Perry R. James, George Karabotsos |
JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar, Jim Woodcock (eds.) |
Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings |
VSTTE |
2008 |
DBLP BibTeX RDF |
|
| 1 | Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, Artem Starostin |
The Verisoft Approach to Systems Verification. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Joey W. Coleman |
Expression Decomposition in a Rely/Guarantee Context. |
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 | K. Rustan M. Leino, Peter Müller, Angela Wallenburg |
Flexible Immutability with Frozen Objects. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Eyad Alkassar, Mark A. Hillebrand |
Formal Functional Verification of Device Drivers. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rafal Kolanski, Gerwin Klein |
Mapped Separation Logic. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | John C. Reynolds |
Readable Formal Proofs. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Colin O'Halloran |
Where Is the Value in a Program Verifier?. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Hubbard, Raimondas Lencevicius, Edu Metz, Gopal Raghavan |
Performance Validation on Multicore Mobile Devices. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfgang Paul |
Towards a Worldwide Verification Technology. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gary T. Leavens, Curtis Clifton |
Lessons from the JML Project. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Yves Bertot, Laurent Théry |
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Utting |
The Role of Model-Based Testing. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Andy Galloway, Frantz Iwu, John A. McDermid, Ian Toyn |
On the Formal Development of Safety-Critical Software. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gogul Balakrishnan, Thomas W. Reps, David Melski, Tim Teitelbaum |
WYSINWYX: What You See Is Not What You eXecute. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou |
Program Verification by Using DISCOVERER. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
semi-algebraic systems, DISCOVERER, reachability computation, program verification, termination, invariant generation |
| 1 | John C. Reynolds |
An Overview of Separation Logic. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Arnaud Venet |
Towards the Integration of Symbolic and Numerical Static Analysis. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramesh Bharadwaj |
Verified Software: The RealGrand Challenge. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | David Evans |
Toasters, Seat Belts, and Inferring Program Properties. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Naumann |
Modular Reasoning in Object-Oriented Programming. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Joshi, Gerard J. Holzmann |
A Mini Challenge: Build a Verifiable Filesystem. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael G. Hinchey, James L. Rash, Christopher A. Rouff |
Some Verification Issues at NASA Goddard Space Flight Center. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, Masami Hagiya |
Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerard J. Holzmann, Rajeev Joshi |
Reliable Software Systems Design: Defect Prevention, Detection, and Containment. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith |
Model Checking: Back and Forth between Hardware and Software. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Mats Per Erik Heimdahl |
A Case for Specification Validation. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Jian Zhang 0001 |
Constraint Solving and Symbolic Execution. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios |
The Challenge of Hardware-Software Co-verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Graham Steel |
The Importance of Non-theorems and Counterexamples in Program Verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Tevfik Bultan, Aysu Betin-Can |
Scalable Software Model Checking Using Design for Verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph R. Kiniry, Patrice Chalin, Clément Hurlin |
Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
A Mechanized Program Verifier. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Schürmann |
Meta-Logical Frameworks and Formal Digital Libraries. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Müller |
Reasoning about Object Structures Using Ownership. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Egon Börger |
Linking the Meaning of Programs to What the Compiler Can Verify. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony Hall |
Software Verification and Software Engineering a Practitioner's Perspective. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Myla Archer |
Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Tony Hoare, Jayadev Misra |
Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | |
The SPARK Team: Languages, Ambiguity, and Verification. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Marsha Chechik, Arie Gurfinkel |
Model-Checking Software Using Precise Abstractions. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Nurit Dor, John Field, Denis Gopan, Tal Lev-Ami, Alexey Loginov, Roman Manevich, G. Ramalingam, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav, Greta Yorsh |
Automatic Verification of Strongly Dynamic Software Systems. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic |
It Is Time to Mechanize Programming Language Metatheory. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Aaron Stump |
Programming with Proofs: Language-Based Approaches to Totally Correct Software. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Kathi Fisler, Shriram Krishnamurthi |
Decomposing Verification Around End-User Features. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")