Application of constraints to formal verification and artificial intelligence

摘要

We are excited to present the AMAI special issue on Application of Constraints to Formal Verification and Artificial Intelligence. The issue contains three papers: In the first paper, entitled Establishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, Monitoring and Learning, Alex Groce from Oregon State University, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi from the NASA Jet Propulsion Laboratory (JPL), and Ru-Gang Xu from the University of California at Los Angeles discuss the application of a range of techniques to the verification of mission-critical flight software at JPL. They present insights on the combination of random testing, model checking, constraint-solving, monitoring, and finite-state machine learning, in addition to static code analysis for the efficient verification of properties of a flash file system and other software for space missions.