A Comprehensive Overview of Formal Methods and Deep Learning for Verification and Optimization

Anand Swaroop, Abhishek Singh, Girish Chandra, Shiv Prakash, Sohan Kumar Yadav, Tiansheng Yang, Rajkumar Singh Rathore

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Formal approaches, which have their roots in logic and mathematics, offer reliable guarantees of the accuracy of software systems. Many strategies have been developed, including model checking, deductive verification, and static analysis. These methods attempt to overcome issues such as undecidability and scalability, which are brought to light by Rice's Theorem and restrict our capacity to develop instruments that can consistently ascertain the correctness of a program. In deductive verification, the work by Floyd, Hoare, and Naur, check program requirements are using logic; nevertheless, further annotations are frequently needed for tractability. Model checking is beneficial for hardware verification and evaluates correctness using temporal logic, but it has trouble with infinite-state systems. By understanding programs at an abstract level, static analysis and abstract interpretation provide completely automated, scalable solutions that detect possible flaws without running the code. In order to overcome the challenge of demonstrating modern architectures like convolutional neural networks (CNNs), the paper also investigates the application of formal approaches to neural networks. The neural network features like resilience and safety against adversarial assaults are verified using techniques like SMT-based approaches and abstract interpretation frameworks like AI2, DeepZ, and DeepPoly. These tools demonstrate the growing importance of formal techniques in ensuring the security and reliability of neural networks, which are being used in more important systems.
Original languageEnglish
Title of host publication2024 International Conference on Decision Aid Sciences and Applications (DASA)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages1-6
Number of pages6
ISBN (Electronic)9798350369106
ISBN (Print)979-8-3503-6911-3
DOIs
Publication statusPublished - 17 Jan 2025
Event2024 International Conference on Decision Aid Sciences and Applications (DASA) - Manama, Bahrain
Duration: 11 Dec 202412 Dec 2024

Publication series

Name2024 International Conference on Decision Aid Sciences and Applications (DASA)
PublisherIEEE Computer Society

Conference

Conference2024 International Conference on Decision Aid Sciences and Applications (DASA)
Country/TerritoryBahrain
CityManama
Period11/12/2412/12/24

Keywords

  • Abstract Interpretation
  • Formal Methods
  • Model Checking
  • Neural Networks
  • SMT

Cite this