Automated reasoning about classical mechanics by Wong, Leon Chih Wen

Get full text

Automated Reasoning About Classical Mechanics by Wong, Leon

Get full text

Lifting Transformations by McAllester, David, Siskind, Jeffrey

Subjects: Get full text

Observations on Cognitive Judgments by McAllester, David

Subjects: Get full text

The Programmer's Apprentice Project: A Research Overview by Rich, Charles, Waters, Richard C.

Subjects: Get full text

Grammar Rewriting by McAllester, David

Subjects: Get full text

Tractable Inference Relations by Givan, Robert, McAllester, David

Subjects: Get full text

Integrated reasoning and proof choice point selection in the jahob system (Mechanisms for program survival) by Rinard, Martin C.

“…In recent years researchers have developed a wide range of powerful automated reasoning systems. We have leveraged these systems to build Jahob, a program specification, analysis, and verification system. …”
Get full text
Get full text

Reasoning Utility Package User's Manual, Version One by McAllester, David Allen

“…In writing all of these utilities an attempt has been made to provide a maximally flexible environment for automated reasoning.…”
Get full text

Verification of full functional correctness for imperative linked data structures by Zee, Karen K

Get full text

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs by Pit-Claudel, Clement Francois, Wang, Peng, Delaware, Benjamin, Gross, Jason S., Chlipala, Adam

Get full text

Pattern-Directed Invocation with Changing Equations by Feldman, Yishai A., Rich, Charles

“…The interaction of pattern-directed invocation with equality in an automated reasoning system gives rise to a completeness problem. …”
Get full text

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs by Pit-Claudel, Clément, Wang, Peng, Delaware, Benjamin, Gross, Jason S., Chlipala, Adam

Get full text

An Integrated Proof Language for Imperative Programs by Zee, Karen, Kuncak, Viktor, Rinard, Martin C.

“…Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems.…”
Get full text
Get full text

Polite Combination of Algebraic Datatypes by Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Lange, Jane, Fontaine, Pascal, Barrett, Clark

“…Abstract Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). …”
Get full text

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq by Gross, Jason, Erbsen, Andres, Philipoom, Jade, Agrawal, Rajashree, Chlipala, Adam

Get full text

Verifying the Performance of Network Control Algorithms by Arun, Venkat

“…Such models allow us to analyze complex system behaviors using automated reasoning techniques. We will present automated tools to analyze congestion control and process scheduling algorithms. …”
Get full text
Get full text

Information extraction to facilitate translation of natural language legislation by Wang, Samuel (Samuel Siyue)

Get full text

Automated security analysis of payment protocols by Huang, Enyang

Get full text

Modular data structure verification by Kuncak, Viktor (Viktor Jaroslav), 1977-

Get full text