Coming to terms with quantified reasoning
- Submitting institution
-
The University of Manchester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 170812208
- Type
- E - Conference contribution
- DOI
-
10.1145/3009837.3009887
- Title of conference / published proceedings
- POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
- First page
- 260
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- January
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
A - Computer Science
- Citation count
- 7
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- First work to incorporate native reasoning with term algebras (an important mathematical technique for representing programs within program verification methods) into a competitive saturation-based automated reasoning tool (Vampire). It laid the foundation for further work in automated structural induction and program verification based on trace logic with a collection of at least 8 further papers published exploring extensions of the work. The first author (Kovacs) recently received an ERC Consolidator Grant (EUR2M, https://informatics.tuwien.ac.at/news/1964) to extend the techniques and the work enabled the second author (Rollibard) to obtain a postdoc position at IMT Atlantique.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
