TY - GEN
T1 - A Comprehensive Overview of Formal Methods and Deep Learning for Verification and Optimization
AU - Swaroop, Anand
AU - Singh, Abhishek
AU - Chandra, Girish
AU - Prakash, Shiv
AU - Yadav, Sohan Kumar
AU - Yang, Tiansheng
AU - Rathore, Rajkumar Singh
N1 - Publisher Copyright:
© 2024 IEEE.
PY - 2025/1/17
Y1 - 2025/1/17
N2 - 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.
AB - 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.
KW - Abstract Interpretation
KW - Formal Methods
KW - Model Checking
KW - Neural Networks
KW - SMT
UR - http://www.scopus.com/inward/record.url?scp=85217263078&partnerID=8YFLogxK
U2 - 10.1109/dasa63652.2024.10836654
DO - 10.1109/dasa63652.2024.10836654
M3 - Conference contribution
SN - 979-8-3503-6911-3
T3 - 2024 International Conference on Decision Aid Sciences and Applications (DASA)
SP - 1
EP - 6
BT - 2024 International Conference on Decision Aid Sciences and Applications (DASA)
PB - Institute of Electrical and Electronics Engineers (IEEE)
T2 - 2024 International Conference on Decision Aid Sciences and Applications (DASA)
Y2 - 11 December 2024 through 12 December 2024
ER -