TY - GEN
T1 - Learning algorithms and formal verification
AU - Madhusudan, P.
PY - 2007/11/27
Y1 - 2007/11/27
N2 - This tutorial is on applications of computational learning theory to verification of systems. Computational learning theory deals with algorithmic models for learning formally representable concepts using either positive and negative samples or by access to an oracle that can answer certain queries about the concept. The problem of learning formal languages has been particularly useful in verification applications. We will introduce Angluin's algorithm, a learning algorithm that learns regular languages efficiently using an oracle that can answer membership and equivalence queries. We will also survey results on learning regular languages in other learning models. We will give an account of how learning has been used to solve a variety of problems in verification, spanning compositional verification, parameterized model-checking, synthesis of interfaces, machines with unbounded queues, and program testing. In all these examples, a crucial property that is exploited is the simplicity of certain concepts that underlie real-world systems, the learning of which yields a a simple mechanism to prove the correctness of the system. We will also lay out general arguments on why learning algorithms can play a crucial role in the design of verification algorithms, and list some open research directions that work towards this goal.
AB - This tutorial is on applications of computational learning theory to verification of systems. Computational learning theory deals with algorithmic models for learning formally representable concepts using either positive and negative samples or by access to an oracle that can answer certain queries about the concept. The problem of learning formal languages has been particularly useful in verification applications. We will introduce Angluin's algorithm, a learning algorithm that learns regular languages efficiently using an oracle that can answer membership and equivalence queries. We will also survey results on learning regular languages in other learning models. We will give an account of how learning has been used to solve a variety of problems in verification, spanning compositional verification, parameterized model-checking, synthesis of interfaces, machines with unbounded queues, and program testing. In all these examples, a crucial property that is exploited is the simplicity of certain concepts that underlie real-world systems, the learning of which yields a a simple mechanism to prove the correctness of the system. We will also lay out general arguments on why learning algorithms can play a crucial role in the design of verification algorithms, and list some open research directions that work towards this goal.
UR - http://www.scopus.com/inward/record.url?scp=36349026912&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=36349026912&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:36349026912
SN - 3540697357
SN - 9783540697350
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
BT - Verification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings
T2 - 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007
Y2 - 14 January 2007 through 16 January 2007
ER -