Intelligent formal methods

  • Information technology has become an indispensable part of our daily lives, with a significant proportion of our everyday activities relying on the safe and reliable operation of computer systems. One promising approach to ensuring these critical properties is the use of so-called formal methods, a broad range of rigorous, mathematical techniques for specifying, developing, and verifying hardware, software, cyber-physical systems, and artificial intelligence. Unlike traditional quality assurance approaches, such as testing, formal methods offer the unique ability to provide formal proof of the absence of errors, a trait particularly desirable in the context of today's ubiquitous safety-critical systems. However, this advantage comes at a cost: formal methods require extensive training, often assume idealized or limited settings, and typically demand substantial computational resources. Inspired by the vision of artificial intelligence, this work seeks to automate formal methods and dramatically expand their applicability. To achieve this goal, we develop a novel, innovative type of formal method that combines inductive techniques from machine learning with deductive techniques from logic. We name this new approach "intelligent formal methods" and apply it to three fundamental areas: software verification, hardware and software synthesis, and the generation of formal specifications.

Download full text files

Export metadata

Author:Daniel NeiderORCiD
Subtitle (English):Combining deductive and inductive reasoning to build reliable systems
Advisor:Daniel Neider
Document Type:Habilitation
Language of publication:English
Date of Publication (online):2022/06/01
Year of first Publication:2022
Publishing Institution:Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau
Granting Institution:Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau
Acceptance Date of the Thesis:2022/06/01
Date of the Publication (Server):2024/05/03
Page Number:V, 116
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):F. Theory of Computation / F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
F. Theory of Computation / F.3 LOGICS AND MEANINGS OF PROGRAMS / F.3.1 Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
F. Theory of Computation / F.3 LOGICS AND MEANINGS OF PROGRAMS / F.3.2 Semantics of Programming Languages (D.3.1) / Program analysis (NEW)
I. Computing Methodologies / I.2 ARTIFICIAL INTELLIGENCE / I.2.6 Learning (K.3.2)
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0)