Specification Inference and Invariant Generation: A Machine Learning Perspective Article Swipe
Computing good specification and invariants is key to effective and efficient program verification. In this talk, I will describe our experiences in using machine learning techniques (Bayesian inference, SVMs) for computing specifications and invariants useful for program verification. The first project Merlin uses Bayesian inference in order to automatically infer security specifications of programs. A novel feature of Merlin is that it can infer specifications even when the code under analysis gives rise to conflicting constraints, a situation that typically occurs when there are bugs. We have used Merlin to infer security specifications of 10 large business critical web applications. Furthermore, we show that these specifications can be used to detect new information flow security vulnerabilities in these applications. In the second project Interpol, we show how interpolants can be viewed as classifiers in supervised machine learning. This view has several advantages: First, we are able to use off-the-shelf classification techniques, in particular support vector machines (SVMs), for interpolation. Second, we show that SVMs can find relevant predicates for a number of benchmarks. Since classification algorithms are predictive, the interpolants computed via classification are likely to be relevant predicates or invariants. Finally, the machine learning view also enables us to handle superficial non-linearities. Even if the underlying problem structure is linear, the symbolic constraints can give an impression that we are solving a non-linear problem. Since learning algorithms try to mine the underlying structure directly, we can discover the linear structure for such problems. We demonstrate the feasibility of Interpol via experiments over benchmarks from various papers on program verification.
Related Topics
Concepts
Metadata
- Type
- article
- Language
- en
- Landing Page
- https://doi.org/10.29007/tx1s
- https://easychair.org/publications/open/5c
- OA Status
- bronze
- Related Works
- 20
- OpenAlex ID
- https://openalex.org/W2403207833
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W2403207833Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.29007/tx1sDigital Object Identifier
- Title
-
Specification Inference and Invariant Generation: A Machine Learning PerspectiveWork title
- Type
-
articleOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2018Year of publication
- Publication date
-
2018-01-23Full publication date if available
- Authors
-
Aditya V. NoriList of authors in order
- Landing page
-
https://doi.org/10.29007/tx1sPublisher landing page
- PDF URL
-
https://easychair.org/publications/open/5cDirect link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
bronzeOpen access status per OpenAlex
- OA URL
-
https://easychair.org/publications/open/5cDirect OA link when available
- Concepts
-
Computer science, Machine learning, Artificial intelligence, Inference, Support vector machine, Bayesian inference, Bayesian probabilityTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
0Total citation count in OpenAlex
- Related works (count)
-
20Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W2403207833 |
|---|---|
| doi | https://doi.org/10.29007/tx1s |
| ids.doi | https://doi.org/10.29007/tx1s |
| ids.mag | 2403207833 |
| ids.openalex | https://openalex.org/W2403207833 |
| fwci | 0.0 |
| type | article |
| title | Specification Inference and Invariant Generation: A Machine Learning Perspective |
| biblio.issue | |
| biblio.volume | 17 |
| biblio.last_page | 52 |
| biblio.first_page | 54 |
| topics[0].id | https://openalex.org/T12423 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9965000152587891 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1712 |
| topics[0].subfield.display_name | Software |
| topics[0].display_name | Software Reliability and Analysis Research |
| topics[1].id | https://openalex.org/T10260 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9948999881744385 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1710 |
| topics[1].subfield.display_name | Information Systems |
| topics[1].display_name | Software Engineering Research |
| topics[2].id | https://openalex.org/T11241 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.9915000200271606 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1711 |
| topics[2].subfield.display_name | Signal Processing |
| topics[2].display_name | Advanced Malware Detection Techniques |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C41008148 |
| concepts[0].level | 0 |
| concepts[0].score | 0.7802382707595825 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[0].display_name | Computer science |
| concepts[1].id | https://openalex.org/C119857082 |
| concepts[1].level | 1 |
| concepts[1].score | 0.7323555946350098 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q2539 |
| concepts[1].display_name | Machine learning |
| concepts[2].id | https://openalex.org/C154945302 |
| concepts[2].level | 1 |
| concepts[2].score | 0.6631929874420166 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q11660 |
| concepts[2].display_name | Artificial intelligence |
| concepts[3].id | https://openalex.org/C2776214188 |
| concepts[3].level | 2 |
| concepts[3].score | 0.6158125996589661 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q408386 |
| concepts[3].display_name | Inference |
| concepts[4].id | https://openalex.org/C12267149 |
| concepts[4].level | 2 |
| concepts[4].score | 0.5783039927482605 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q282453 |
| concepts[4].display_name | Support vector machine |
| concepts[5].id | https://openalex.org/C160234255 |
| concepts[5].level | 3 |
| concepts[5].score | 0.4138844907283783 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q812535 |
| concepts[5].display_name | Bayesian inference |
| concepts[6].id | https://openalex.org/C107673813 |
| concepts[6].level | 2 |
| concepts[6].score | 0.3395811915397644 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q812534 |
| concepts[6].display_name | Bayesian probability |
| keywords[0].id | https://openalex.org/keywords/computer-science |
| keywords[0].score | 0.7802382707595825 |
| keywords[0].display_name | Computer science |
| keywords[1].id | https://openalex.org/keywords/machine-learning |
| keywords[1].score | 0.7323555946350098 |
| keywords[1].display_name | Machine learning |
| keywords[2].id | https://openalex.org/keywords/artificial-intelligence |
| keywords[2].score | 0.6631929874420166 |
| keywords[2].display_name | Artificial intelligence |
| keywords[3].id | https://openalex.org/keywords/inference |
| keywords[3].score | 0.6158125996589661 |
| keywords[3].display_name | Inference |
| keywords[4].id | https://openalex.org/keywords/support-vector-machine |
| keywords[4].score | 0.5783039927482605 |
| keywords[4].display_name | Support vector machine |
| keywords[5].id | https://openalex.org/keywords/bayesian-inference |
| keywords[5].score | 0.4138844907283783 |
| keywords[5].display_name | Bayesian inference |
| keywords[6].id | https://openalex.org/keywords/bayesian-probability |
| keywords[6].score | 0.3395811915397644 |
| keywords[6].display_name | Bayesian probability |
| language | en |
| locations[0].id | doi:10.29007/tx1s |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4220651395 |
| locations[0].source.issn | 2398-7340 |
| locations[0].source.type | journal |
| locations[0].source.is_oa | False |
| locations[0].source.issn_l | 2398-7340 |
| locations[0].source.is_core | True |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | EPiC series in computing |
| locations[0].source.host_organization | |
| locations[0].source.host_organization_name | |
| locations[0].license | |
| locations[0].pdf_url | https://easychair.org/publications/open/5c |
| locations[0].version | publishedVersion |
| locations[0].raw_type | proceedings-article |
| locations[0].license_id | |
| locations[0].is_accepted | True |
| locations[0].is_published | True |
| locations[0].raw_source_name | EPiC Series in Computing |
| locations[0].landing_page_url | https://doi.org/10.29007/tx1s |
| locations[1].id | mag:2403207833 |
| locations[1].is_oa | False |
| locations[1].source | |
| locations[1].license | |
| locations[1].pdf_url | |
| locations[1].version | |
| locations[1].raw_type | |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | https://dblp.uni-trier.de/db/conf/cade/atx-wing2012.html#Nori12 |
| indexed_in | crossref |
| authorships[0].author.id | https://openalex.org/A5111937381 |
| authorships[0].author.orcid | |
| authorships[0].author.display_name | Aditya V. Nori |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Aditya V. Nori |
| authorships[0].is_corresponding | True |
| has_content.pdf | True |
| has_content.grobid_xml | True |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://easychair.org/publications/open/5c |
| open_access.oa_status | bronze |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Specification Inference and Invariant Generation: A Machine Learning Perspective |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T03:46:38.306776 |
| primary_topic.id | https://openalex.org/T12423 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9965000152587891 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1712 |
| primary_topic.subfield.display_name | Software |
| primary_topic.display_name | Software Reliability and Analysis Research |
| related_works | https://openalex.org/W2968438543, https://openalex.org/W3036006055, https://openalex.org/W1758923908, https://openalex.org/W2891160484, https://openalex.org/W1933411530, https://openalex.org/W1549615248, https://openalex.org/W3125159057, https://openalex.org/W2511174833, https://openalex.org/W2913613828, https://openalex.org/W2973588525, https://openalex.org/W654937010, https://openalex.org/W3140654866, https://openalex.org/W3021083399, https://openalex.org/W2970746059, https://openalex.org/W2243053057, https://openalex.org/W2593925740, https://openalex.org/W3200653887, https://openalex.org/W326099964, https://openalex.org/W3021068062, https://openalex.org/W2496170334 |
| cited_by_count | 0 |
| locations_count | 2 |
| best_oa_location.id | doi:10.29007/tx1s |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4220651395 |
| best_oa_location.source.issn | 2398-7340 |
| best_oa_location.source.type | journal |
| best_oa_location.source.is_oa | False |
| best_oa_location.source.issn_l | 2398-7340 |
| best_oa_location.source.is_core | True |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | EPiC series in computing |
| best_oa_location.source.host_organization | |
| best_oa_location.source.host_organization_name | |
| best_oa_location.license | |
| best_oa_location.pdf_url | https://easychair.org/publications/open/5c |
| best_oa_location.version | publishedVersion |
| best_oa_location.raw_type | proceedings-article |
| best_oa_location.license_id | |
| best_oa_location.is_accepted | True |
| best_oa_location.is_published | True |
| best_oa_location.raw_source_name | EPiC Series in Computing |
| best_oa_location.landing_page_url | https://doi.org/10.29007/tx1s |
| primary_location.id | doi:10.29007/tx1s |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4220651395 |
| primary_location.source.issn | 2398-7340 |
| primary_location.source.type | journal |
| primary_location.source.is_oa | False |
| primary_location.source.issn_l | 2398-7340 |
| primary_location.source.is_core | True |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | EPiC series in computing |
| primary_location.source.host_organization | |
| primary_location.source.host_organization_name | |
| primary_location.license | |
| primary_location.pdf_url | https://easychair.org/publications/open/5c |
| primary_location.version | publishedVersion |
| primary_location.raw_type | proceedings-article |
| primary_location.license_id | |
| primary_location.is_accepted | True |
| primary_location.is_published | True |
| primary_location.raw_source_name | EPiC Series in Computing |
| primary_location.landing_page_url | https://doi.org/10.29007/tx1s |
| publication_date | 2018-01-23 |
| publication_year | 2018 |
| referenced_works_count | 0 |
| abstract_inverted_index.A | 54 |
| abstract_inverted_index.I | 16 |
| abstract_inverted_index.a | 76, 169, 222 |
| abstract_inverted_index.10 | 94 |
| abstract_inverted_index.In | 13, 119 |
| abstract_inverted_index.We | 85, 244 |
| abstract_inverted_index.an | 216 |
| abstract_inverted_index.as | 131 |
| abstract_inverted_index.be | 107, 129, 186 |
| abstract_inverted_index.if | 204 |
| abstract_inverted_index.in | 21, 45, 116, 133, 151 |
| abstract_inverted_index.is | 5, 59, 209 |
| abstract_inverted_index.it | 61 |
| abstract_inverted_index.of | 52, 57, 93, 171, 248 |
| abstract_inverted_index.on | 257 |
| abstract_inverted_index.or | 189 |
| abstract_inverted_index.to | 7, 47, 73, 89, 109, 146, 185, 199, 229 |
| abstract_inverted_index.us | 198 |
| abstract_inverted_index.we | 101, 124, 143, 160, 219, 235 |
| abstract_inverted_index.The | 38 |
| abstract_inverted_index.and | 3, 9, 32 |
| abstract_inverted_index.are | 83, 144, 176, 183, 220 |
| abstract_inverted_index.can | 62, 106, 128, 164, 214, 236 |
| abstract_inverted_index.for | 29, 35, 157, 168, 241 |
| abstract_inverted_index.has | 139 |
| abstract_inverted_index.how | 126 |
| abstract_inverted_index.key | 6 |
| abstract_inverted_index.new | 111 |
| abstract_inverted_index.our | 19 |
| abstract_inverted_index.the | 67, 120, 178, 192, 205, 211, 231, 238, 246 |
| abstract_inverted_index.try | 228 |
| abstract_inverted_index.use | 147 |
| abstract_inverted_index.via | 181, 250 |
| abstract_inverted_index.web | 98 |
| abstract_inverted_index.Even | 203 |
| abstract_inverted_index.SVMs | 163 |
| abstract_inverted_index.This | 137 |
| abstract_inverted_index.able | 145 |
| abstract_inverted_index.also | 196 |
| abstract_inverted_index.code | 68 |
| abstract_inverted_index.even | 65 |
| abstract_inverted_index.find | 165 |
| abstract_inverted_index.flow | 113 |
| abstract_inverted_index.from | 254 |
| abstract_inverted_index.give | 215 |
| abstract_inverted_index.good | 1 |
| abstract_inverted_index.have | 86 |
| abstract_inverted_index.mine | 230 |
| abstract_inverted_index.over | 252 |
| abstract_inverted_index.rise | 72 |
| abstract_inverted_index.show | 102, 125, 161 |
| abstract_inverted_index.such | 242 |
| abstract_inverted_index.that | 60, 78, 103, 162, 218 |
| abstract_inverted_index.this | 14 |
| abstract_inverted_index.used | 87, 108 |
| abstract_inverted_index.uses | 42 |
| abstract_inverted_index.view | 138, 195 |
| abstract_inverted_index.when | 66, 81 |
| abstract_inverted_index.will | 17 |
| abstract_inverted_index.SVMs) | 28 |
| abstract_inverted_index.Since | 173, 225 |
| abstract_inverted_index.bugs. | 84 |
| abstract_inverted_index.first | 39 |
| abstract_inverted_index.gives | 71 |
| abstract_inverted_index.infer | 49, 63, 90 |
| abstract_inverted_index.large | 95 |
| abstract_inverted_index.novel | 55 |
| abstract_inverted_index.order | 46 |
| abstract_inverted_index.talk, | 15 |
| abstract_inverted_index.there | 82 |
| abstract_inverted_index.these | 104, 117 |
| abstract_inverted_index.under | 69 |
| abstract_inverted_index.using | 22 |
| abstract_inverted_index.First, | 142 |
| abstract_inverted_index.Merlin | 41, 58, 88 |
| abstract_inverted_index.detect | 110 |
| abstract_inverted_index.handle | 200 |
| abstract_inverted_index.likely | 184 |
| abstract_inverted_index.linear | 239 |
| abstract_inverted_index.number | 170 |
| abstract_inverted_index.occurs | 80 |
| abstract_inverted_index.papers | 256 |
| abstract_inverted_index.second | 121 |
| abstract_inverted_index.useful | 34 |
| abstract_inverted_index.vector | 154 |
| abstract_inverted_index.viewed | 130 |
| abstract_inverted_index.(SVMs), | 156 |
| abstract_inverted_index.Second, | 159 |
| abstract_inverted_index.enables | 197 |
| abstract_inverted_index.feature | 56 |
| abstract_inverted_index.linear, | 210 |
| abstract_inverted_index.machine | 23, 135, 193 |
| abstract_inverted_index.problem | 207 |
| abstract_inverted_index.program | 11, 36, 258 |
| abstract_inverted_index.project | 40, 122 |
| abstract_inverted_index.several | 140 |
| abstract_inverted_index.solving | 221 |
| abstract_inverted_index.support | 153 |
| abstract_inverted_index.various | 255 |
| abstract_inverted_index.Bayesian | 43 |
| abstract_inverted_index.Finally, | 191 |
| abstract_inverted_index.Interpol | 249 |
| abstract_inverted_index.analysis | 70 |
| abstract_inverted_index.business | 96 |
| abstract_inverted_index.computed | 180 |
| abstract_inverted_index.critical | 97 |
| abstract_inverted_index.describe | 18 |
| abstract_inverted_index.discover | 237 |
| abstract_inverted_index.learning | 24, 194, 226 |
| abstract_inverted_index.machines | 155 |
| abstract_inverted_index.problem. | 224 |
| abstract_inverted_index.relevant | 166, 187 |
| abstract_inverted_index.security | 50, 91, 114 |
| abstract_inverted_index.symbolic | 212 |
| abstract_inverted_index.(Bayesian | 26 |
| abstract_inverted_index.Computing | 0 |
| abstract_inverted_index.Interpol, | 123 |
| abstract_inverted_index.computing | 30 |
| abstract_inverted_index.directly, | 234 |
| abstract_inverted_index.effective | 8 |
| abstract_inverted_index.efficient | 10 |
| abstract_inverted_index.inference | 44 |
| abstract_inverted_index.learning. | 136 |
| abstract_inverted_index.problems. | 243 |
| abstract_inverted_index.programs. | 53 |
| abstract_inverted_index.situation | 77 |
| abstract_inverted_index.structure | 208, 233, 240 |
| abstract_inverted_index.typically | 79 |
| abstract_inverted_index.algorithms | 175, 227 |
| abstract_inverted_index.benchmarks | 253 |
| abstract_inverted_index.impression | 217 |
| abstract_inverted_index.inference, | 27 |
| abstract_inverted_index.invariants | 4, 33 |
| abstract_inverted_index.non-linear | 223 |
| abstract_inverted_index.particular | 152 |
| abstract_inverted_index.predicates | 167, 188 |
| abstract_inverted_index.supervised | 134 |
| abstract_inverted_index.techniques | 25 |
| abstract_inverted_index.underlying | 206, 232 |
| abstract_inverted_index.advantages: | 141 |
| abstract_inverted_index.benchmarks. | 172 |
| abstract_inverted_index.classifiers | 132 |
| abstract_inverted_index.conflicting | 74 |
| abstract_inverted_index.constraints | 213 |
| abstract_inverted_index.demonstrate | 245 |
| abstract_inverted_index.experiences | 20 |
| abstract_inverted_index.experiments | 251 |
| abstract_inverted_index.feasibility | 247 |
| abstract_inverted_index.information | 112 |
| abstract_inverted_index.invariants. | 190 |
| abstract_inverted_index.predictive, | 177 |
| abstract_inverted_index.superficial | 201 |
| abstract_inverted_index.techniques, | 150 |
| abstract_inverted_index.Furthermore, | 100 |
| abstract_inverted_index.constraints, | 75 |
| abstract_inverted_index.interpolants | 127, 179 |
| abstract_inverted_index.applications. | 99, 118 |
| abstract_inverted_index.automatically | 48 |
| abstract_inverted_index.off-the-shelf | 148 |
| abstract_inverted_index.specification | 2 |
| abstract_inverted_index.verification. | 12, 37, 259 |
| abstract_inverted_index.classification | 149, 174, 182 |
| abstract_inverted_index.interpolation. | 158 |
| abstract_inverted_index.specifications | 31, 51, 64, 92, 105 |
| abstract_inverted_index.vulnerabilities | 115 |
| abstract_inverted_index.non-linearities. | 202 |
| cited_by_percentile_year | |
| corresponding_author_ids | https://openalex.org/A5111937381 |
| countries_distinct_count | 0 |
| institutions_distinct_count | 1 |
| citation_normalized_percentile.value | 0.00684647 |
| citation_normalized_percentile.is_in_top_1_percent | False |
| citation_normalized_percentile.is_in_top_10_percent | False |