kirancodes.me
To Proof Maintenance & Beyond!
Venues / VMCAI /

VMCAI 2021

26 papers

  1. A Design of GPU-Based Quantitative Model Checking · YoungMin Kwon, Eunhee Kim
  2. A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries · Nathalie Bertrand, Marijana Lazic, Josef Widder
  3. A Self-certifying Compilation Framework for WebAssembly · Kedar S. Namjoshi, Anton Xue
  4. A Synchronous Effects Logic for Temporal Verification of Pure Esterel · Yahui Song, Wei-Ngan Chin
  5. Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) · Andreas Humenberger, Laura Kovács
  6. Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible · Marius Kamp, Michael Philippsen
  7. Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis · Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin
  8. Compositional Model Checking for Multi-properties · Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald
  9. Compositional Satisfiability Solving in Separation Logic · Quang Loc Le
  10. Concurrent Correctness in Vector Space · Christina L. Peterson, Victor Cook, Damian Dechev
  11. Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories · Martin Bromberger, Alberto Fiori, Christoph Weidenbach
  12. Decomposing Data Structure Commutativity Proofs with $m\!n$-Differencing · Eric Koskinen, Kshitij Bansal
  13. Eliminating Message Counters in Synchronous Threshold Automata · Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
  14. Formal Semantics and Verification of Network-Based Biocomputation Circuits · Michelle Aluf-Medina, Till Korten, Avraham Raviv, Dan V. Nicolau Jr., Hillel Kugler
  15. GPURepair: Automated Repair of GPU Kernels · Saurabh Joshi, Gautam Muduganti
  16. Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper) · Bernhard Steffen, Alnis Murtovi
  17. Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching · Jochen Hoenicke, Tanja Schindler
  18. Model Checking Algorithms for Hyperproperties (Invited Paper) · Bernd Finkbeiner
  19. Netter: Probabilistic, Stateful Network Models · Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, Limin Jia
  20. On Preprocessing for Weighted MaxSAT · Tobias Paxian, Pascal Raiola, Bernd Becker
  21. Proving the Existence of Fair Paths in Infinite-State Systems · Alessandro Cimatti, Alberto Griggio, Enrico Magnago
  22. Runtime Abstract Interpretation for Numerical Accuracy and Robustness · Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles
  23. Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking · Hongce Zhang, Aarti Gupta, Sharad Malik
  24. Twinning Automata and Regular Expressions for String Static Analysis · Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi
  25. Unbounded Procedure Summaries from Bounded Environments · Lauren Pick, Grigory Fedyukovich, Aarti Gupta
  26. Verification of Concurrent Programs Using Petri Net Unfoldings · Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schätzle