researchr
explore
Tags
Journals
Conferences
Authors
Profiles
Groups
calendar
New Conferences
Events
Deadlines
search
search
You are not signed in
Sign in
Sign up
Links
Filter by Year
OR
AND
NOT
1
2005
2008
2010
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
Filter by Tag
[+]
OR
AND
NOT
1
C++
Java
Meta-Environment
abstraction
analysis
compiler
context-aware
design
logic
meta-model
meta-objects
model checking
program verification
programming
programming languages
refinement
reuse
rule-based
systematic-approach
testing
Filter by Author
[+]
OR
AND
NOT
1
Andrei Paskevich
Alessandro Coglio
Andreas Podelski
Anindya Banerjee
Arie Gurfinkel
Artem Starostin
Bernhard Beckert
Bertrand Meyer
Burkhart Wolff
Carsten Sinz
Claude Marché
David A. Naumann
Eyad Alkassar
Gerhard Schellhorn
Jean-Christophe Filliâtre
K. Rustan M. Leino
Martin Clochard
Mattias Ulbrich
Serdar Tasiran
Viktor Kuncak
Filter by Top terms
[+]
OR
AND
NOT
1
analysis
checking
conference
experiments
formal
international
model
papers
program
programs
proofs
revised
selected
software
theories
tools
using
verification
verified
vstte
VSTTE (vstte)
Editions
Publications
Viewing Publication 1 - 100 from 269
2023
Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers
Akash Lal
,
Stefano Tonetta
, editors,
Volume 13800 of
Lecture Notes in Computer Science
, Springer,
2023.
[doi]
2022
Compositional Safety LTL Synthesis
Suguman Bansal
,
Giuseppe De Giacomo
,
Antonio Di Stasio 0001
,
Yong Li 0031
,
Moshe Y. Vardi
,
Shufang Zhu 0001
.
vstte 2023
:
1-19
[doi]
Leroy and Blazy Were Right: Their Memory Model Soundness Proof is Automatable
Pedro Barroso
,
Mário Pereira
,
António Ravara
.
vstte 2023
:
20-32
[doi]
Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers
Roderick Bloem
,
Rayna Dimitrova
,
Chuchu Fan
,
Natasha Sharygina
, editors,
Volume 13124 of
Lecture Notes in Computer Science
, Springer,
2022.
[doi]
Shellac: A Compiler Synthesizer for Concurrent Programs
Christopher K. Chen
,
Margo I. Seltzer
,
Mark R. Greenstreet
.
vstte 2023
:
33-51
[doi]
A Sequentialization Procedure for Fault-Tolerant Protocols
Cezara Dragoi
,
Patricio Inzaghi Pronesti
.
vstte 2023
:
52-71
[doi]
Towards Practical Partial Order Reduction for High-Level Formalisms
Philipp Körner
,
Michael Leuschel
.
vstte 2023
:
72-91
[doi]
SMT-Based Verification of Persistency Invariants of Px86 Programs
Iason Marmanis
,
Viktor Vafeiadis
.
vstte 2023
:
92-110
[doi]
A Formal Semantics for P-Code
Nico Naus
,
Freek Verbeek
,
Dale Walker
,
Binoy Ravindran
.
vstte 2023
:
111-128
[doi]
Separating Separation Logic - Modular Verification of Red-Black Trees
Gerhard Schellhorn
,
Stefan Bodenmüller
,
Martin Bitterlich
,
Wolfgang Reif
.
vstte 2023
:
129-147
[doi]
Residual Runtime Verification via Reachability Analysis
Chukri Soueidi
,
Yliès Falcone
.
vstte 2023
:
148-166
[doi]
2021
Partial Order Reduction for Timed Actors
Maryam Bagheri 0001
,
Marjan Sirjani
,
Ehsan Khamespanah
,
Hossein Hojjat
,
Ali Movaghar 0001
.
vstte 2022
:
43-60
[doi]
Uncertainty-Aware Signal Temporal Logic Inference
Nasim Baharisangari
,
Jean-Raphaël Gaglione
,
Daniel Neider
,
Ufuk Topcu
,
Zhe Xu 0005
.
vstte 2022
:
61-85
[doi]
An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods
Farah Benmouhoub
,
Pierre-Loïc Garoche
,
Matthieu Martel
.
vstte 2022
:
165-181
[doi]
A Calculus for Multi-language Operational Semantics
Matteo Cimini
.
vstte 2022
:
25-42
[doi]
Making Proofs of Floating-Point Programs Accessible to Regular Developers
Claire Dross
,
Johannes Kanig
.
vstte 2022
:
7-24
[doi]
Formal Verification of Neural Network Controllers for Collision-Free Flight
Daniel Genin
,
Ivan Papusha
,
Joshua Brulé
,
Tyler Young
,
Galen E. Mullins
,
Yanni Kouskoulas
,
Rosa Wu
,
Aurora C. Schmidt
.
vstte 2022
:
147-164
[doi]
Abstract Interpretation of LLVM with a Region-Based Memory Model
Arie Gurfinkel
,
Jorge A. Navas
.
vstte 2022
:
122-144
[doi]
Quantitative Monitoring of Software
Thomas A. Henzinger
.
vstte 2022
:
3-6
[doi]
Case Study: Analysis of Autonomous Center Line Tracking Neural Networks
Ismet Burak Kadron
,
Divya Gopinath
,
Corina S. Pasareanu
,
Huafeng Yu
.
vstte 2022
:
104-121
[doi]
Designing and Proving Properties of the Abaco Autoscaler Using TLA+
Smruti Padhy
,
Joe Stubbs
.
vstte 2022
:
86-103
[doi]
Modeling Round-Off Errors in Hydrodynamic Simulations
William Weens
,
Thibaud Vazquez-Gonzalez
,
Louise Ben Salem-Knapp
.
vstte 2022
:
182-196
[doi]
2020
Automatic Detection and Repair of Transition- Based Leakage in Software Binaries
Konstantinos Athanasiou
,
Thomas Wahl
,
A. Adam Ding
,
Yunsi Fei
.
vstte 2020
:
50-67
[doi]
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya
,
Sydney Gibson
,
Yao Li
,
Bryan Parno
,
Chris Hawblitzel
.
vstte 2020
:
106-123
[doi]
QPR Verify: A Static Analysis Tool for Embedded Software Based on Bounded Model Checking
Marko Kleine Büning
,
Carsten Sinz
,
David Faragó
.
vstte 2020
:
21-32
[doi]
Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers
Supratik Chakraborty
,
Jorge A. Navas
, editors,
Volume 12031 of
Lecture Notes in Computer Science
, Springer,
2020.
[doi]
Software Verification - 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers
Maria Christakis
,
Nadia Polikarpova
,
Parasara Sridhar Duggirala
,
Peter Schrammel
, editors,
Volume 12549 of
Lecture Notes in Computer Science
, Springer,
2020.
[doi]
SARL: OO Framework Specification for Static Analysis
Pietro Ferrara
,
Luca Negrini
.
vstte 2020
:
3-20
[doi]
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
Mikhail R. Gadelha
,
Lucas C. Cordeiro
,
Denis A. Nicole
.
vstte 2020
:
178-195
[doi]
Rigorous Enclosure of Round-Off Errors in Floating-Point Computations
Rémy Garcia
,
Claude Michel
,
Michel Rueher
.
vstte 2020
:
196-212
[doi]
Can We Avoid Rounding-Error Estimation in HPC Codes and Still Get Trustworthy Results?
Fabienne Jézéquel
,
Stef Graillat
,
Daichi Mukunoki
,
Toshiyuki Imamura
,
Roman Iakymchuk
.
vstte 2020
:
163-177
[doi]
Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants
Bibek Kabi
,
Eric Goubault
,
Antoine Miné
,
Sylvie Putot
.
vstte 2020
:
221-238
[doi]
MCBAT: Model Counting for Constraints over Bounded Integer Arrays
Abtin Molavi
,
Tommy Schneider
,
Mara Downing
,
Lucas Bang
.
vstte 2020
:
124-143
[doi]
Verification of an Optimized NTT Algorithm
Jorge A. Navas
,
Bruno Dutertre
,
Ian A. Mason
.
vstte 2020
:
144-160
[doi]
Towards Numerical Assistants - Trust, Measurement, Community, and Generality for the Numerical Workbench
Pavel Panchekha
,
Zachary Tatlock
.
vstte 2020
:
213-220
[doi]
BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers
Joseph Scott
,
Federico Mora
,
Vijay Ganesh
.
vstte 2020
:
68-86
[doi]
Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison
Alessandro Trindade
,
Lucas C. Cordeiro
.
vstte 2020
:
87-105
[doi]
Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX
Vadim Zaliva
,
Ilia Zaichuk
,
Franz Franchetti
.
vstte 2020
:
33-49
[doi]
2019
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
Yuepeng Wang 0001
,
Shuvendu K. Lahiri
,
Shuo Chen
,
Rong Pan
,
Isil Dillig
,
Cody Born
,
Immad Naseer
,
Kostas Ferles
.
vstte 2020
:
87-106
[doi]
Ghost Code in Action: Automated Verification of a Symbolic Interpreter
Benedikt Becker
,
Claude Marché
.
vstte 2020
:
107-123
[doi]
Quantifying Information Leakage Using Model Counting Constraint Solvers
Tevfik Bultan
.
vstte 2020
:
30-35
[doi]
Uncertainty, Modeling and Safety Assurance: Towards a Unified Framework
Marsha Chechik
,
Sahar Kokaly
,
Mona Rahimi
,
Rick Salay
,
Torin Viger
.
vstte 2020
:
19-29
[doi]
Intersection and Rotation of Assumption Literals Boosts Bug-Finding
Rohit Dureja
,
Jianwen Li
,
Geguang Pu
,
Moshe Y. Vardi
,
Kristin Y. Rozier
.
vstte 2020
:
180-192
[doi]
Seamless Interactive Program Verification
Sarah Grebing
,
Jonas Klamroth
,
Mattias Ulbrich
.
vstte 2020
:
68-86
[doi]
Verifiable Homomorphic Tallying for the Schulze Vote Counting Scheme
Thomas Haines
,
Dirk Pattinson
,
Mukesh Tiwari
.
vstte 2020
:
36-53
[doi]
Incremental Minimization of Symbolic Automata
Jonathan Homburg
,
Parasara Sridhar Duggirala
.
vstte 2020
:
54-67
[doi]
Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer
Matthieu Journault
,
Antoine Miné
,
Raphaël Monat
,
Abdelraouf Ouadjaout
.
vstte 2020
:
1-18
[doi]
Refinement Type Contracts for Verification of Scientific Investigative Software
Maxwell Shinn
.
vstte 2020
:
143-160
[doi]
DCSynth: Guided Reactive Synthesis with Soft Requirements
Amol Wakankar
,
Paritosh K. Pandya
,
Raj Mohan Matteplackel
.
vstte 2020
:
124-142
[doi]
solc-verify: A Modular Verifier for Solidity Smart Contracts
Ákos Hajdu
,
Dejan Jovanovic
.
vstte 2020
:
161-179
[doi]
2018
Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity
Jakub Zakrzewski 0001
.
vstte 2018
:
229-247
[doi]
Loop Detection by Logically Constrained Term Rewriting
Naoki Nishida 0001
,
Sarah Winkler
.
vstte 2018
:
309-321
[doi]
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components
Robin Adams
,
Sibylle Schupp
.
vstte 2018
:
196-214
[doi]
SideTrail: Verifying Time-Balancing of Cryptosystems
Konstantinos Athanasiou
,
Byron Cook
,
Michael Emmi
,
Colm MacCárthaigh
,
Daniel Schwartz-Narbonne
,
Serdar Tasiran
.
vstte 2018
:
215-228
[doi]
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Bernhard Beckert
,
Timo Bingmann
,
Moritz Kiefer
,
Peter Sanders 0001
,
Mattias Ulbrich
,
Alexander Weigl
.
vstte 2018
:
248-266
[doi]
TWAM: A Certifying Abstract Machine for Logic Programs
Brandon Bohrer
,
Karl Crary
.
vstte 2018
:
112-134
[doi]
Verification of Binarized Neural Networks via Inter-neuron Factoring - (Short Paper)
Chih-Hong Cheng
,
Georg Nührenberg
,
Chung-Hao Huang
,
Harald Ruess
.
vstte 2018
:
279-290
[doi]
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Alessandro Coglio
.
vstte 2018
:
177-195
[doi]
Practical Methods for Reasoning About Java 8's Functional Programming Features
David R. Cok
,
Serdar Tasiran
.
vstte 2018
:
267-278
[doi]
A Java Bytecode Formalisation
Patryk Czarnik
,
Jacek Chrzaszcz
,
Aleksy Schubert
.
vstte 2018
:
135-154
[doi]
The Map Equality Domain
Daniel Dietsch
,
Matthias Heizmann
,
Jochen Hoenicke
,
Alexander Nutz
,
Andreas Podelski
.
vstte 2018
:
291-308
[doi]
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications
Hugo Férée
,
Johannes Åman Pohjola
,
Ramana Kumar
,
Scott Owens
,
Magnus O. Myreen
,
Son Ho
.
vstte 2018
:
88-111
[doi]
Executable Counterexamples in Software Model Checking
Jeffrey Gennari
,
Arie Gurfinkel
,
Temesghen Kahsai
,
Jorge A. Navas
,
Edward J. Schwartz
.
vstte 2018
:
17-37
[doi]
Verified Certificate Checking for Counting Votes
Milad K. Ghale
,
Dirk Pattinson
,
Ramana Kumar
,
Michael Norrish
.
vstte 2018
:
69-87
[doi]
A Tree-Based Approach to Data Flow Proofs
Jochen Hoenicke
,
Alexander Nutz
,
Andreas Podelski
.
vstte 2018
:
1-16
[doi]
Lattice-Based Refinement in Bounded Model Checking
Karine Even Mendoza
,
Sepideh Asadi
,
Antti E. J. Hyvärinen
,
Hana Chockler
,
Natasha Sharygina
.
vstte 2018
:
50-68
[doi]
Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment
Jonas Oberhauser
.
vstte 2018
:
322-344
[doi]
Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers
Ruzica Piskac
,
Philipp Rümmer
, editors,
Volume 11294 of
Lecture Notes in Computer Science
, Springer,
2018.
[doi]
Extending VIAP to Handle Array Programs
Pritom Rajkhowa
,
Fangzhen Lin
.
vstte 2018
:
38-49
[doi]
Formalising Executable Specifications of Low-Level Systems
Paolo Torrini
,
David Nowak
,
Narjes Jomaa
,
Mohamed Sami Cherif
.
vstte 2018
:
155-176
[doi]
2017
Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models
Tatsuya Abe 0001
,
Tomoharu Ugawa
,
Toshiyuki Maeda
.
vstte 2017
:
170-190
[doi]
Proving JDK's Dual Pivot Quicksort Correct
Bernhard Beckert
,
Jonas Schiffl
,
Peter H. Schmitt
,
Mattias Ulbrich
.
vstte 2017
:
35-48
[doi]
A Semi-automatic Proof of Strong Connectivity
Ran Chen
,
Jean-Jacques Lévy
.
vstte 2017
:
49-65
[doi]
A Formal Analysis of the Compact Position Reporting Algorithm
Aaron Dutle
,
Mariano M. Moscato
,
Laura Titolo
,
César A. Muñoz
.
vstte 2017
:
19-34
[doi]
Automating the Verification of Floating-Point Programs
Clément Fumex
,
Claude Marché
,
Yannick Moy
.
vstte 2017
:
102-119
[doi]
A Formally Verified Interpreter for a Shell-Like Programming Language
Nicolas Jeannerod
,
Claude Marché
,
Ralf Treinen
.
vstte 2017
:
1-18
[doi]
Practical Void Safety
Alexander Kogtenkov
.
vstte 2017
:
132-151
[doi]
Memory-Efficient Tactics for Randomized LTL Model Checking
Kim G. Larsen
,
Doron Peled
,
Sean Sedwards
.
vstte 2017
:
152-169
[doi]
Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions
Saeed Nejati
,
Jia Hui Liang
,
Catherine H. Gebotys
,
Krzysztof Czarnecki
,
Vijay Ganesh
.
vstte 2017
:
120-131
[doi]
An Abstraction Technique for Describing Concurrent Program Behaviour
Wytse Oortwijn
,
Stefan Blom
,
Dilian Gurov
,
Marieke Huisman
,
Marina Zaharieva-Stojanovski
.
vstte 2017
:
191-209
[doi]
Verified Software. Theories, Tools, and Experiments - 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers
Andrei Paskevich
,
Thomas Wies
, editors,
Volume 10712 of
Lecture Notes in Computer Science
, Springer,
2017.
[doi]
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
Raphaël Rieu-Helft
,
Claude Marché
,
Guillaume Melquiond
.
vstte 2017
:
84-101
[doi]
Verifying Branch-Free Assembly Code in Why3
Marc Schoolderman
.
vstte 2017
:
66-83
[doi]
2016
SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms
Dirk Beyer 0001
,
Matthias Dangl
.
vstte 2016
:
181-198
[doi]
Verified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers
Sandrine Blazy
,
Marsha Chechik
, editors,
Volume 9971 of
Lecture Notes in Computer Science
,
2016.
[doi]
The Matrix Reproved (Verification Pearl)
Martin Clochard
,
Léon Gondelman
,
Mário Pereira
.
vstte 2016
:
107-118
[doi]
Constructing Semantic Models of Programs with the Software Analysis Workbench
Robert Dockins
,
Adam Foltzer
,
Joe Hendrix
,
Brian Huffman
,
Dylan McNamee
,
Aaron Tomb
.
vstte 2016
:
56-72
[doi]
Producing All Ideals of a Forest, Formally (Verification Pearl)
Jean-Christophe Filliâtre
,
Mário Pereira
.
vstte 2016
:
46-55
[doi]
Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers
Arie Gurfinkel
,
Sanjit A. Seshia
, editors,
Volume 9593 of
Lecture Notes in Computer Science
, Springer,
2016.
[doi]
Resolution in Solving Graph Problems
Kailiang Ji
.
vstte 2016
:
166-180
[doi]
JavaSMT: A Unified Interface for SMT Solvers in Java
Egor George Karpenkov
,
Karlheinz Friedberger
,
Dirk Beyer 0001
.
vstte 2016
:
139-148
[doi]
Relational Program Reasoning Using Compiler IR
Moritz Kiefer
,
Vladimir Klebanov
,
Mattias Ulbrich
.
vstte 2016
:
149-165
[doi]
Automated Verification of Functional Correctness of Race-Free GPU Programs
Kensuke Kojima
,
Akifumi Imanishi
,
Atsushi Igarashi
.
vstte 2016
:
90-106
[doi]
Stupid Tool Tricks for Smart Model Based Design
Mark Lawford
.
vstte 2016
:
1-7
[doi]
Order Reduction for Multi-core Interruptible Operating Systems
Jonas Oberhauser
.
vstte 2016
:
27-45
[doi]
Specification: The Biggest Bottleneck in Formal Methods and Autonomy
Kristin Yvonne Rozier
.
vstte 2016
:
8-26
[doi]
Accelerating the General Simplex Procedure for Linear Real Arithmetic via GPUs
Steven T. Stewart
,
Derek Rayside
,
Vijay Ganesh
,
Krzysztof Czarnecki
.
vstte 2016
:
129-138
[doi]
Bidirectional Grammars for Machine-Code Decoding and Encoding
Gang Tan
,
Greg Morrisett
.
vstte 2016
:
73-89
[doi]
Enabling Modular Verification with Abstract Interference Specifications for a Concurrent Queue
Alan Weide
,
Paolo A. G. Sivilotti
,
Murali Sitaraman
.
vstte 2016
:
119-128
[doi]
2015
Moving Around: Lipton's Reduction for TSO - (Regular Submission)
Ali Sezgin
,
Serdar Tasiran
.
vstte 2016
:
165-182
[doi]
Sign in
or
sign up
to see more results.