English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Horn-ICE Learning for Synthesizing Invariants and Contracts

D'Souza, D., Ezudheen, P., Garg, P., Madhusudan, P., & Neider, D. (2017). Horn-ICE Learning for Synthesizing Invariants and Contracts. Retrieved from http://arxiv.org/abs/1712.09418.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/21.11116/0000-0000-765A-7 Version Permalink: https://hdl.handle.net/21.11116/0000-0000-765B-6
Genre: Paper

Files

show Files
hide Files
:
arXiv:1712.09418.pdf (Preprint), 291KB
View   Save
File Permalink:
https://hdl.handle.net/21.11116/0000-0000-765C-5
Name:
arXiv:1712.09418.pdf
Description:
File downloaded from arXiv at 2018-02-13 11:22
OA-Status:
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
View
Copyright Date:
-
Copyright Info:
-
License:
http://arxiv.org/help/license

Locators

show

Creators

show
hide
 Creators:
D'Souza, Deepak1, Author
Ezudheen, P.1, Author
Garg, Pranav1, Author
Madhusudan, P.1, Author
Neider, Daniel2, Author           
Affiliations:
1External Organizations, ou_persistent22              
2Group R. Majumdar, Max Planck Institute for Software Systems, Max Planck Society, ou_2105292              

Content

show
hide
Free keywords: Computer Science, Logic in Computer Science, cs.LO,Computer Science, Learning, cs.LG,Computer Science, Programming Languages, cs.PL,
 Abstract: We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.

Details

show
hide
Language(s): eng - English
 Dates: 2017-12-262017
 Publication Status: Published online
 Pages: 18 S.
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: arXiv: 1712.09418
URI: http://arxiv.org/abs/1712.09418
BibTex Citekey: Neider2017c
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show