More Web Proxy on the site http://driver.im/

research-article

Open access

Modelling program verification tools for software engineers

Authors:

Sophie Lathouwers,

Vadim ZaytsevAuthors Info & Claims

MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems

Pages 98 - 108

https://doi.org/10.1145/3550355.3552426

Published: 24 October 2022 Publication History

Abstract

In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools, and present a concise megamodel to distinguish these tools. We also present a data set of almost 400 program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links, and more. The categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set, publicly available at https://doi.org/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements.

References

[1]

Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr, and Tomáš Vojnar. 2010. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer, 132--147.

Digital Library

[2]

Aws Albarghouthi, Loris D'Antoni, and Samuel Drews. 2017. Repairing Decision-Making Programs Under Uncertainty. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV), Rupak Majumdar and Viktor Kunčak (Eds.). Springer, 181--200.

[3]

Matthew Amy, Martin Roetteler, and Krysta M. Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), Rupak Majumdar and Viktor Kunčak (Eds.). Springer, 3--21.

[4]

Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2018. Let this Graph Be Your Witness!. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV), Hana Chockler and Georg Weissenbacher (Eds.). Springer, 3--11.

[5]

Pranav Ashok, Mathias Jackermeier, Jan Křetínský, Christoph Weinhuber, Maximilian Weininger, and Mayank Yadav. 2021. dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. In Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer, Cham, 326--345.

Digital Library

[6]

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized Metatheory for the Masses: The PoplMark Challenge. In Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs) (LNCS, Vol. 3603), Joe Hurd and Thomas F. Melham (Eds.). Springer, 50--65.

Digital Library

[7]

Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch, and Julian Siber. 2021. Causality-Based Game Solving. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, Cham, 894--917.

Digital Library

[8]

Gianluca Barbon, Vincent Leroy, and Gwen Salaün. 2019. Debugging of Behavioural Models with CLEAR. In Tools and Algorithms for the Construction and Analysis of Systems, Tomáš Vojnar and Lijun Zhang (Eds.). Springer, 386--392.

Digital Library

[9]

Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. 2018. Model Checking Indistinguishability of Randomized Security Protocols. In Computer Aided Verification (CAV), Hana Chockler and Georg Weissenbacher (Eds.). Springer, 117--135.

[10]

Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 1996. UPPAAL: A Tool Suite for Automatic Verification of Real-Time Systems. In Hybrid Systems III, Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag (Eds.). Springer, 232--243.

[11]

Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer Berlin, Heidelberg, London.

[12]

Dirk Beyer. 2022. Progress on Software Verification: SV-COMP 2022. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer, Cham, 375--402.

Digital Library

[13]

Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, 184--190.

[14]

Juan Bicarregui, C. A. R. Hoare, and J. C. P. Woodcock. 2006. The Verified Software Repository: A Step Towards the Verifying Compiler. Formal Aspects of Computing 18, 2 (2006), 143--151.

Digital Library

[15]

Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, and Gilles Muller. 2005. Formal Methods Meet Domain Specific Languages. In Proceedings of the Fifth International Conference on Integrated Formal Methods (iFM) (LNCS, Vol. 3771), Judi Romijn, Graeme Smith, and Jaco van de Pol (Eds.). Springer, 187--206.

Digital Library

[16]

Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2017. Proving Termination Through Conditional Termination. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer, 99--117.

[17]

Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. 2017. MightyL: A Compositional Translation from MITL to Timed Automata. In Computer Aided Verification, Rupak Majumdar and Viktor Kunčak (Eds.). Springer, 421--440.

[18]

Guy H. Broadfoot and Philippa J. Broadfoot. 2003. Academia and Industry Meet: Some Experiences of Formal Methods in Practice. In Proceedings of the 10th Asia-Pacific Software Engineering Conference (APSEC). IEEE Computer Society, 49.

[19]

Antonio Bucchiarone, Federico Ciccozzi, Leen Lambers, Alfonso Pierantonio, Matthias Tichy, Massimo Tisi, Andreas Wortmann, and Vadim Zaytsev. 2021. What is the Future of Modelling? IEEE Software Insights (IEEE Software) 38 (2021), 119--127. Issue 2.

Digital Library

[20]

Géraud Canet, Pascal Cuoq, and Benjamin Monate. 2009. A Value Analysis for C Programs. In Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2009, Edmonton, Alberta, Canada, September 20--21, 2009. IEEE Computer Society, 123--124.

Digital Library

[21]

Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, and Zhibin Yang. 2016. Parametric Runtime Verification of C Programs. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-François Raskin (Eds.). Springer, 299--315.

[22]

Jennifer A. Davis, Matthew A. Clark, Darren D. Cofer, Aaron Fifarek, Jacob Hinchman, Jonathan A. Hoffman, Brian W. Hulbert, Steven P. Miller, and Lucas G. Wagner. 2013. Study on the Barriers to the Industrial Adoption of Formal Methods. In Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) (LNCS, Vol. 8187), Charles Pecheur and Michael Dierkes (Eds.). Springer, 63--77.

Digital Library

[23]

Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS, Vol. 4963), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, 337--340.

[24]

Adel Djoudi and Sébastien Bardin. 2015. BINSEC: Binary Code Analysis with Low-Level Regions. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS, Vol. 9035), Christel Baier and Cesare Tinelli (Eds.). Springer, 212--217.

Digital Library

[25]

Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, and Peter Müller. 2018. Permission Inference for Array Programs. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer, 55--74.

[26]

Samuel Drews, Aws Albarghouthi, and Loris D'Antoni. 2019. Efficient Synthesis with Probabilistic Constraints. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV), Isil Dillig and Serdar Tasiran (Eds.). Springer, 278--296.

[27]

Gidon Ernst and Toby Murray. 2019. SecCSL: Security Concurrent Separation Logic. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer, 208--230.

[28]

Hugues Evrard. 2016. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-François Raskin (Eds.). Springer, 553--559.

Digital Library

[29]

Yliès Falcone, Srdan Krstic, Giles Reger, and Dmitriy Traytel. 2021. A Taxonomy for Classifying Runtime Verification Tools. International Journal on Software Tools for Technology Transfer 23, 2 (2021), 255--284.

Digital Library

[30]

Alessio Ferrari, Franco Mazzanti, Davide Basile, Maurice H. ter Beek, and Alessandro Fantechi. 2020. Comparing Formal Tools for System Design: A Judgment Study. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE '20). Association for Computing Machinery, 62--74.

Digital Library

[31]

Martin Fowler. 2005. Language Workbenches: The Killer-App for Domain Specific Languages? MartinFowler.com. https://martinfowler.com/articles/languageWorkbench.html

[32]

Georg Frey and Lothar Litz. 2000. Formal Methods in PLC Programming. In Proceedings of the International Conference on Systems, Man & Cybernetics: "Cybernetics Evolving to Systems, Humans, Organizations, and their Complex Interactions". IEEE, 2431--2436.

[33]

Shafi Goldwasser, Silvio Micali, and Charles Rackoff. 1985. The Knowledge Complexity of Interactive Proof-Systems. In Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (SToC) (STOC). Association for Computing Machinery, 291--304.

Digital Library

[34]

Kiran Gopinathan and Ilya Sergey. 2020. Certifying Certainty and Uncertainty in Approximate Membership Query Structures. In Computer Aided Verification (CAV), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 279--303.

Digital Library

[35]

Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, and Zhong Shao. 2019. Integrating Formal Schedulability Analysis into a Verified OS Kernel. In Computer Aided Verification (CAV), Isil Dillig and Serdar Tasiran (Eds.). Springer, 496--514.

[36]

Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, and Enno Ruijters. 2019. The Quantitative Verification Benchmark Set. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS, Vol. 11427), Tomás Vojnar and Lijun Zhang (Eds.). Springer, 344--350.

Digital Library

[37]

Dominik Harz and William J. Knottenbelt. 2018. Towards Safer Smart Contracts: A Survey of Languages and Verification Methods. CoRR abs/1809.09805 (2018), 20 pages. arXiv:1809.09805 http://arxiv.org/abs/1809.09805

[38]

Mostafa Hassan, Caterina Urban, Marco Eilers, and Peter Müller. 2018. MaxSMT-Based Type Inference for Python 3. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer, 12--19.

[39]

Lukáš Holík, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Jiří Šimáček, and Tomáš Vojnar. 2017. Forester: From Heap Shapes to Automata Predicates. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer, 365--369.

[40]

John Edward Hutchinson, Jon Whittle, and Mark Rouncefield. 2014. Model-Driven Engineering Practices in Industry: Social, Organizational and Managerial Factors that Lead to Success or Failure. Science of Computer Programming 89 (2014), 144--161.

Digital Library

[41]

Sung-Shik T. Q. Jongmans and Farhad Arbab. 2016. PrDK: Protocol Programming with Automata. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-François Raskin (Eds.). Springer, 547--552.

Digital Library

[42]

René Klösch and Wolfgang Eixelsberger. 1999. Challenges and Experiences in Managing Major Software Evolution Endeavours Such as Euro Conversion or Y2000 Compliance. In Proceedings of the 15th International Conference on Software Maintenance (ICSM). IEEE Computer Society, 161--166.

[43]

Martin Kölbl, Stefan Leue, and Thomas Wies. 2020. TarTar: A Timed Automata Repair Tool. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 529--540.

[44]

Laura Kovács and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer, 1--35.

[45]

Leslie Lamport. 1994. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems (ToPLaS) 16, 3 (1994), 872--923.

Digital Library

[46]

Jianwen Li, Moshe Y. Vardi, and Kristin Y. Rozier. 2019. Satisfiability Checking for Mission-Time LTL. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer, 3--22.

[47]

Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, and Clark W. Barrett. 2021. Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. In SAT 2021 (LNCS, Vol. 12831), Chu-Min Li and Felip Manyà (Eds.). Springer, 377--386.

[48]

Wim Meeus, Kristof Van Beeck, Toon Goedemé, Jan Meel, and Dirk Stroobandt. 2012. An overview of today's high-level synthesis tools. Des. Autom. Embed. Syst. 16, 3 (2012), 31--51.

Digital Library

[49]

Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Proceddings of the 28th International Conference on Automated Deduction (CADE), André Platzer and Geoff Sutcliffe (Eds.). Springer, 625--635.

Digital Library

[50]

Jan Mrázek, Petr Bauch, Henrich Lauko, and Jiří Barnat. 2016. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Model Checking Software, Dragan Bošnački and Anton Wijs (Eds.). Springer, 208--213.

[51]

Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng, and Zhen Zhang. 2019. STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer, 540--549.

[52]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson (Eds.). 2002. 5. The Rules of the Game. Springer, 67--104.

[53]

Arif Nurwidyantoro, Mojtaba Shahin, Michel Chaudron, Waqar Hussain, Harsha Perera, Rifat Ara Shams, and Jon Whittle. 2021. Towards a Human Values Dashboard for Software Development: An Exploratory Study. In Proceedings of the 15th International Symposium on Empirical Software Engineering and Measurement (ESEM), Filippo Lanubile, Marcos Kalinowski, and Maria Teresa Baldassarre (Eds.). ACM, 23:1--23:12.

Digital Library

[54]

Arif Nurwidyantoro, Mojtaba Shahin, Michel R. V. Chaudron, Waqar Hussain, Rifat Ara Shams, Harsha Perera, Gillian Oliver, and Jon Whittle. 2022. Human Values in Software Development Artefacts: A Case Study on Issue Discussions in Three Android Applications. Information & Software Technology 141 (2022), 106731.

Digital Library

[55]

T. Parr. 2013. The Definitive ANTLR 4 Reference. Pragmatic Bookshelf. https://books.google.nl/books?id=gA9QDwAAQBAJ

[56]

Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, and David Chemouil. 2021. Sound Verification Procedures for Temporal Properties of Infinite-State Systems. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 337--360.

Digital Library

[57]

Amir Pnueli. 1977. The Temporal Logic of Programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, 46--57.

Digital Library

[58]

Ratish J. Punnoose, Robert C. Armstrong, Matthew H. Wong, and Mayo Jackson. 2014. Survey of Existing Tools for Formal Verification. Technical Report. USDOE National Nuclear Security Administration (NNSA).

[59]

Cedric Richter and Heike Wehrheim. 2019. PeSCo: Predicting Sequential Combinations of Verifiers. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer, 229--233.

[60]

Bat-Chen Rothenberg and Orna Grumberg. 2020. Must Fault Localization for Program Repair. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 658--680.

[61]

Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Dan, and Martin Vechev. 2021. Scalable Polyhedral Verification of Recurrent Neural Networks. In Computer Aided Verification (CAV, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 225--248.

Digital Library

[62]

Rupert Schlick, Michael Felderer, István Majzik, Roberto Nardone, Alexander Raschke, Colin F. Snook, and Valeria Vittorini. 2018. A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods. In Proceedings of the Eighth International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) (LNCS, Vol. 11247), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 249--272.

Digital Library

[63]

Abdelkader Magdy Shaaban, Christoph Schmittner, Thomas Gruber, A. Baith Mohamed, Gerald Quirchmayr, and Erich Schikuta. 2019. Ontology-Based Model for Automotive Security Verification and Validation. In Proceedings of the 21st International Conference on Information Integration and Web-based Applications & Services (iiWAS). ACM, 73--82.

Digital Library

[64]

Aleksey Shipilëv. 2013. Java Concurrency Stress (jcstress). https://github.com/openjdk/jcstress/.

[65]

Herbert Stachowiak. 1973. Allgemeine Modelltheorie. Springer.

[66]

Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2016. MU-CSeq 0.4: Individual Memory Location Unwindings. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-François Raskin (Eds.). Springer, 938--941.

[67]

Federico Tomassetti and Vadim Zaytsev. 2020. Reflections on the Lack of Adoption of Domain Specific Languages. In STAF Workshop Proceedings (STAF) (CEUR Workshop Proceedings, Vol. 2707), Loli Burgueño and Lars Michael Kristensen (Eds.). CEUR-WS.org, 85--94. http://ceur-ws.org/Vol-2707/oopslepaper5.pdf

[68]

Muhammad Usman, Divya Gopinath, Youcheng Sun, Yannic Noller, and Corina S. Păsăreanu. 2021. NNrepair: Constraint-Based Repair of Neural Network Classifiers. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 3--25.

[69]

Tom van Dijk. 2018. Oink: An Implementation and Evaluation of Modern Parity Game Solvers. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Dirk Beyer and Marieke Huisman (Eds.), Vol. 10805. Springer, 291--308.

[70]

Jon Whittle, Maria Angela Ferrario, Will Simm, and Waqar Hussain. 2021. A Case for Human Values in Software Engineering. IEEE Software 38, 1 (2021), 106--113.

Digital Library

[71]

Freek Wiedijk. 2003. Comparing Mathematical Provers. In Proceedings of the Second International Conference on Mathematical Knowledge Management (MKM) (LNCS, Vol. 2594), Andrea Asperti, Bruno Buchberger, and James H. Davenport (Eds.). Springer, 188--202.

[72]

Avi Wigderson. 2019. Mathematics and Computation: Ideas Revolutionizing Technology and Science. Princeton University Press. https://www.math.ias.edu/avi/book

[73]

Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, and Peter Müller. 2021. Gobra: Modular Specification and Verification of Go Programs. In Proceedings of the 33rd International Conference on Computer Aided Verification (CAV) (LNCS, Vol. 12759), Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 367--379.

Digital Library

[74]

Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. 2009. Formal Methods: Practice and Experience. Comput. Surveys 41, 4 (2009), 19:1--19:36.

Digital Library

[75]

Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. 2008. SATzilla: Portfolio-based Algorithm Selection for SAT. Journal of Artificial Intelligence Research 32 (2008), 565--606.

Cited By

Eberhardinger MRupp FMaucher JMaghsudi S(2024)Unveiling the Decision-Making Process in Reinforcement Learning with Genetic ProgrammingAdvances in Swarm Intelligence10.1007/978-981-97-7181-3_28(349-365)Online publication date: 22-Aug-2024
https://dl.acm.org/doi/10.1007/978-981-97-7181-3_28

Index Terms

Modelling program verification tools for software engineers

Recommendations

Using DEv-PROMELA for Modelling and Verification of Software
SIGSIM-PADS '16: Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation

Efficient modelling and verification of models need an accurate representation of systems. Especially, PROMELA cannot represent time as quantitative properties. That means some properties depending on time cannot be checked with SPIN model-checker. ...
Formal Verification for C Program

Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...
An Interface Theory for Program Verification
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles
Abstract
Program verification is the problem, for a given program and a specification , of constructing a proof of correctness for the statement “program satisfies specification ” () or a proof of violation ([inline-graphic not available: see fulltext]). ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems

October 2022

412 pages

ISBN:9781450394666

DOI:10.1145/3550355

General Chairs:
Eugene Syriani
Université de Montréal, Canada
,
Houari Sahraoui
Université de Montréal, Canada

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

Univ. of Montreal: University of Montreal
IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

MODELS '22

Sponsor:

SIGSOFT

MODELS '22: ACM/IEEE 25th International Conference on Model Driven Engineering Languages and Systems

October 23 - 28, 2022

Quebec, Montreal, Canada

Acceptance Rates

MODELS '22 Paper Acceptance Rate 35 of 125 submissions, 28%;

Overall Acceptance Rate 144 of 506 submissions, 28%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
485
Total Downloads

Downloads (Last 12 months)199
Downloads (Last 6 weeks)20

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Eberhardinger MRupp FMaucher JMaghsudi S(2024)Unveiling the Decision-Making Process in Reinforcement Learning with Genetic ProgrammingAdvances in Swarm Intelligence10.1007/978-981-97-7181-3_28(349-365)Online publication date: 22-Aug-2024
https://dl.acm.org/doi/10.1007/978-981-97-7181-3_28

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents