Higher-Order MSL Horn Constraints

Jerome C Jochems; Eddie C Jones; Steven Ramsay

doi:10.1145/3571262

Higher-Order MSL Horn Constraints

Jerome C Jochems, Eddie C Jones, Steven Ramsay^*

^*Corresponding author for this work

Research output: Contribution to journal › Article (Academic Journal) › peer-review

58 Downloads (Pure)

Abstract

The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.

Original language	English
Article number	69
Pages (from-to)	2017–2047
Number of pages	31
Journal	Proceedings of the ACM on Programming Languages
Volume	7
Issue number	POPL
DOIs	https://doi.org/10.1145/3571262
Publication status	Published - 11 Jan 2023

Bibliographical note

Funding Information:
We gratefully acknowledge the support of the Engineering and Physical Sciences Research Council (EP/T006595/1) and the National Centre for Cyber Security via the UK Research Institute in Verified Trustworthy Software Systems. We are also very grateful for the help of the reviewers in making the paper more clear and accurate, and for suggesting related work.

Publisher Copyright:
© 2023 Owner/Author.

Research Groups and Themes

Programming Languages

Access to Document

10.1145/3571262Licence: CC BY

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Association for Computing Machinery at https://doi.org/10.1145/3571262 . Please refer to any applicable terms of use of the publisher.
Final published version, 360 KBLicence: CC BY

Handle.net

Persistent link

8030 EPSRC EP/T006595/1 Higher-order Constrained Horn Clauses
Ramsay, S.
1/03/20 → 28/02/23
Project: Research

Cite this

@article{515a604886b6424e86920e6e19b4d647,

title = "Higher-Order MSL Horn Constraints",

abstract = "The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.",

author = "Jochems, {Jerome C} and Jones, {Eddie C} and Steven Ramsay",

note = "Funding Information: We gratefully acknowledge the support of the Engineering and Physical Sciences Research Council (EP/T006595/1) and the National Centre for Cyber Security via the UK Research Institute in Verified Trustworthy Software Systems. We are also very grateful for the help of the reviewers in making the paper more clear and accurate, and for suggesting related work. Publisher Copyright: {\textcopyright} 2023 Owner/Author.",

year = "2023",

month = jan,

day = "11",

doi = "10.1145/3571262",

language = "English",

volume = "7",

pages = "2017–2047",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - Higher-Order MSL Horn Constraints

AU - Jochems, Jerome C

AU - Jones, Eddie C

AU - Ramsay, Steven

N1 - Funding Information: We gratefully acknowledge the support of the Engineering and Physical Sciences Research Council (EP/T006595/1) and the National Centre for Cyber Security via the UK Research Institute in Verified Trustworthy Software Systems. We are also very grateful for the help of the reviewers in making the paper more clear and accurate, and for suggesting related work. Publisher Copyright: © 2023 Owner/Author.

PY - 2023/1/11

Y1 - 2023/1/11

N2 - The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.

AB - The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.

U2 - 10.1145/3571262

DO - 10.1145/3571262

M3 - Article (Academic Journal)

SN - 2475-1421

VL - 7

SP - 2017

EP - 2047

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 69

ER -

Higher-Order MSL Horn Constraints

Abstract

Bibliographical note

Research Groups and Themes

Access to Document

Handle.net

Fingerprint

Projects

8030 EPSRC EP/T006595/1 Higher-order Constrained Horn Clauses

Cite this