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

VMCAI 2024

30 papers

  1. A Fully Verified Persistency Library · Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
  2. A Navigation Logic for Recursive Programs with Dynamic Thread Creation · Roman Lakenbrink, Markus Müller-Olm, Christoph Ohrem, Jens Oliver Gutsfeld
  3. AGNES: Abstraction-Guided Framework for Deep Neural Networks Security · Akshay Dhonthi, Marcello Eiermann, Ernst Moritz Hahn, Vahid Hashemi
  4. Abstract Interpretation-Based Feature Importance for Support Vector Machines · Abhinandan Pal, Francesco Ranzato, Caterina Urban, Marco Zanella
  5. Automatic and Incremental Repair for Speculative Information Leaks · Joachim Bard, Swen Jacobs, Yakir Vizel
  6. Automatically Enforcing Rust Trait Properties · Twain Byrnes, Yoshiki Takashima, Limin Jia
  7. Boosting Constrained Horn Solving by Unsat Core Learning · Parosh Aziz Abdulla, Chencheng Liang, Philipp Rümmer
  8. Borrowable Fractional Ownership Types for Verification · Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi
  9. Correctness Witness Validation by Abstract Interpretation · Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, Vesal Vojdani
  10. Deductive Verification of Parameterized Embedded Systems Modeled in SystemC · Philip Tasche, Raúl E. Monti, Stefanie Eva Drerup, Pauline Blohm, Paula Herber, Marieke Huisman
  11. Efficient Local Search for Nonlinear Real Arithmetic · Zhonghan Wang, Bohua Zhan, Bohan Li, Shaowei Cai
  12. Formal Runtime Error Detection During Development in the Automotive Industry · Jesko Hecking-Harbusch, Jochen Quante, Maximilian Schlund
  13. Function Synthesis for Maximizing Model Counting · Thomas Vigouroux, Marius Bozga, Cristian Ene, Laurent Mounier
  14. Generation of Violation Witnesses by Under-Approximating Abstract Interpretation · Marco Milanese, Antoine Miné
  15. Generic Model Checking for Modal Fixpoint Logics in COOL-MC · Daniel Hausmann, Merlin Humml, Simon Prucker, Lutz Schröder, Aaron Strahlberger
  16. Guaranteed Inference for Probabilistic Programs: A Parallelisable, Small-Step Operational Approach · Michele Boreale, Luisa Collodi
  17. Interpolation and Quantifiers in Ortholattices · Simon Guilloud, Sankalp Gambhir, Viktor Kuncak
  18. Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs · Yuxin Deng, Huiling Wu, Ming Xu
  19. Model-Guided Synthesis for LTL over Finite Traces · Shengping Xiao, Yongkang Li, Xinyue Huang, Yicong Xu, Jianwen Li, Geguang Pu + 2 more
  20. On the Verification of the Correctness of a Subgraph Construction Algorithm · Lucas Böltz, Viorica Sofronie-Stokkermans, Hannes Frey
  21. Parameterized Verification of Disjunctive Timed Networks · Étienne André, Paul Eichler, Swen Jacobs, Shyam Lal Karra
  22. Petrification: Software Model Checking for Programs with Dynamic Thread Management · Matthias Heizmann, Dominik Klumpp, Lars Nitzke, Frank Schüssele
  23. Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability · Nicolas Amat, Silvano Dal-Zilio, Didier Le Botlan
  24. Resilience and Home-Space for WSTS · Alain Finkel, Mathieu Hilaire
  25. Solving Two-Player Games Under Progress Assumptions · Anne-Kathrin Schmuck, K. S. Thejaswini, Irmak Saglam, Satya Prakash Nayak
  26. Sound Abstract Nonexploitability Analysis · Francesco Parolini, Antoine Miné
  27. Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic · Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider, Guillermo A. Pérez
  28. TP-DejaVu: Combining Operational and Declarative Runtime Verification · Klaus Havelund, Panagiotis Katsaros, Moran Omer, Doron Peled, Anastasios Temperekidis
  29. Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training · Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Guy Katz, Min Zhang
  30. Verification of Neural Networks' Local Differential Classification Privacy · Roie Reshef, Anan Kabaha, Olga Seleznova, Dana Drachsler-Cohen