English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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