Two Easy Theories Whose Combination is Hard

By V. Pratt. 2002

103 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Handbook of Satisfiability (2021, methodology): “It has been observed [131, 123, 59] that formulas arising in software verification have:”
The octagon abstract domain (2001, unknown): “All these works are based on the concept of shortest-path closure already present in Pratt’s article [7] as the base of the satisﬁability algorithm for constraints of the form ( x − y ≤ c ) .”
A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities (2000, methodology): “We expect that standard analysis techniques (such as SSA form [13], Pratt’s method [49] or Shostak’s loop residues [56], and a points-to analysis) could be used to improve on our current prototype by an order of magnitude or more.”