Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis

Details Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis

2012-01-04

arxiv.org/abs/1201.0979v1

Computer Science

Logic in Computer Science

Scientific paper

Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing and energy consumption, and the automatic synthesis of systems from specifications. The major challenges include environment modeling, incompleteness in specifications, and the complexity of underlying decision problems. This position paper proposes sciduction, an approach to tackle these challenges by integrating inductive inference, deductive reasoning, and structure hypotheses. Deductive reasoning, which leads from general rules or concepts to conclusions about specific problem instances, includes techniques such as logical inference and constraint solving. Inductive inference, which generalizes from specific instances to yield a concept, includes algorithmic learning from examples. Structure hypotheses are used to define the class of artifacts, such as invariants or program fragments, generated during verification or synthesis. Sciduction constrains inductive and deductive reasoning using structure hypotheses, and actively combines inductive and deductive reasoning: for instance, deductive techniques generate examples for learning, and inductive reasoning is used to guide the deductive engines. We illustrate this approach with three applications: (i) timing analysis of software; (ii) synthesis of loop-free programs, and (iii) controller synthesis for hybrid systems. Some future applications are also discussed.

Affiliated with

Also associated with

No associations

Rating

Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-156984