Search

Your search keyword '"Ridge, Tom"' showing total 342 results
Start Over Author "Ridge, Tom"
342 results on '"Ridge, Tom"'

1. Visualizing the Evaluation of Functional Programs for Debugging

Author

Whitington, John and Ridge, Tom

Subjects
Computer Science - Programming Languages, D.2.5
Abstract

In this position paper, we present a prototype of a visualizer for functional programs. Such programs, whose evaluation model is the reduction of an expression to a value through repeated application of rewriting rules, and which tend to make little or no use of mutable state, are amenable to visualization in the same fashion as simple mathematical expressions, with which every schoolchild is familiar. We show how such visualizations may be produced for the strict functional language OCaml, by direct interpretation of the abstract syntax tree and appropriate pretty-printing. We describe (and begin to address) the challenges of presenting such program traces in limited space and of identifying their essential elements, so that our methods will one day be practical for more than toy programs. We consider the problems posed by the parts of modern functional programming which are not purely functional such as mutable state, input/output and exceptions. We describe initial work on the use of such visualizations to address the problem of program debugging, which is our ultimate aim., Comment: 8 pages, 1 figure. arXiv admin note: text overlap with arXiv:1905.06545

Published
2024

4. Direct Interpretation of Functional Programs for Debugging

Author

Whitington, John and Ridge, Tom

Subjects
Computer Science - Programming Languages, Computer Science - Software Engineering, D.2.5
Abstract

We make another assault on the longstanding problem of debugging. After exploring why debuggers are not used as widely as one might expect, especially in functional programming environments, we define the characteristics of a debugger which make it usable and thus widely used. We present initial work towards a new debugger for OCaml which operates by direct interpretation of the program source, allowing the printing out of individual steps of the program's evaluation. We present OCamli, a standalone interpreter, and propose a mechanism by which the interpreter could be integrated into compiled executables, allowing part of a program to be interpreted in the same fashion as OCamli whilst the rest of the program runs natively. We show how such a mechanism might create a source-level debugging system that has the characteristics of a usable debugger (such as being independent of its environment) and so may eventually be expected to be suitable for widespread adoption., Comment: In Proceedings ML 2017, arXiv:1905.05909

Published
2019
Full Text
View/download PDF

5. Contributors

Author

Badel, Pierre, primary, Beeckman, Dimitri, additional, Berke, Christine Thies, additional, Black, Joyce Marie, additional, Blume-Peytavi, Ulrike, additional, Bogie, Kath M., additional, Bonod, Christelle, additional, Brienza, David, additional, Bucki, M., additional, Call, Evan, additional, Chassagne, Fanette, additional, Cheney, Adam, additional, Corrias, Alberto, additional, Demers, Alex, additional, Dror, Y., additional, Fleming, Leigh Toni, additional, Freeman, A., additional, Friedman, Rinat, additional, Fromy, Bérengère, additional, Garcia-Martinez, Daniel, additional, Gefen, Amit, additional, Golberg, Alexander, additional, Gupta, Priyanka, additional, Guzman, Sandra, additional, Kottner, Jan, additional, Krieger, Louis W.M. M., additional, Kumar, Bipin, additional, Leung, Pak Hung, additional, Leyva-Mendivil, Maria Fabiola, additional, Limbert, Georges, additional, Molimard, Jérôme, additional, Narayana, Hairshkumar, additional, Niroomandi, S., additional, Ophir, C., additional, Pan, Ning, additional, Payan, Yohan, additional, Perrier, A., additional, Remoué, Noelle, additional, Ridge, Tom, additional, Scalamandré, Ana, additional, Shabshin, Noga, additional, Shankr, Pramod, additional, Sigaudo-Roussel, Dominique, additional, Soh, Bryan Wee Siang, additional, Sparks, Jessica L., additional, Tucker-Kellogg, Lisa, additional, Vermolen, F.J., additional, Vishwanath, Karthik, additional, Vogt, Annika, additional, and Weihs, Daphne, additional

Published
2020
Full Text
View/download PDF

7. Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL

Author

Ridge, Tom

Subjects
Computer Science - Logic in Computer Science
Abstract

We formalise and mechanise a construtive, proof theoretic proof of Craig's Interpolation Theorem in Isabelle/HOL. We give all the definitions and lemma statements both formally and informally. We also transcribe informally the formal proofs. We detail the main features of our mechanisation, such as the formalisation of binding for first order formulae. We also give some applications of Craig's Interpolation Theorem.

Published
2006

8. Simple, Efficient, Sound and Complete Combinator Parsing for All Context-Free Grammars, Using an Oracle

Author

Ridge, Tom, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Combemale, Benoît, editor, Pearce, David J., editor, Barais, Olivier, editor, and Vinju, Jurgen J., editor

Published
2014
Full Text
View/download PDF

9. Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars

Author

Ridge, Tom, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Jouannaud, Jean-Pierre, editor, and Shao, Zhong, editor

Published
2011
Full Text
View/download PDF

10. The 1st Verified Software Competition: Experience Report

Author

Klebanov, Vladimir, Müller, Peter, Shankar, Natarajan, Leavens, Gary T., Wüstholz, Valentin, Alkassar, Eyad, Arthan, Rob, Bronish, Derek, Chapman, Rod, Cohen, Ernie, Hillebrand, Mark, Jacobs, Bart, Leino, K. Rustan M., Monahan, Rosemary, Piessens, Frank, Polikarpova, Nadia, Ridge, Tom, Smans, Jan, Tobies, Stephan, Tuerk, Thomas, Ulbrich, Mattias, Weiß, Benjamin, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Butler, Michael, editor, and Schulte, Wolfram, editor

Published
2011
Full Text
View/download PDF

11. A Rely-Guarantee Proof System for x86-TSO

Author

Ridge, Tom, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Leavens, Gary T., editor, O’Hearn, Peter, editor, and Rajamani, Sriram K., editor

Published
2010
Full Text
View/download PDF

12. A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service

Author

Ridge, Tom, Norrish, Michael, Sewell, Peter, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cuellar, Jorge, editor, Maibaum, Tom, editor, and Sere, Kaisa, editor

Published
2008
Full Text
View/download PDF

13. Operational Reasoning for Concurrent Caml Programs and Weak Memory Models

Author

Ridge, Tom, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Schneider, Klaus, editor, and Brandt, Jens, editor

Published
2007
Full Text
View/download PDF

14. A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic

Author

Ridge, Tom, Margetson, James, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Hurd, Joe, editor, and Melham, Tom, editor

Published
2005
Full Text
View/download PDF

15. Engineering with Logic.

Author

Bishop, Steve, Fairbairn, Matthew, Mehnert, Hannes, Norrish, Michael, Ridge, Tom, Sewell, Peter, Smith, Michael, and Wansbrough, Keith

Subjects
COMPUTER engineering, DEBUGGING, TCP/IP, AUTOMATION, SOFTWARE engineering
Abstract

Conventional computer engineering relies on test-and-debug development processes, with the behavior of common interfaces described (at best) with prose specification documents. But prose specifications cannot be used in test-and-debug development in any automated way, and prose is a poor medium for expressing complex (and loose) specifications. The TCP/IP protocols and Sockets API are a good example of this: they play a vital role in modern communication and computation, and interoperability between implementations is essential. But what exactly they are is surprisingly obscure: their original development focused on "rough consensus and running code," augmented by prose RFC specifications that do not precisely define what it means for an implementation to be correct. Ultimately, the actual standard is the de facto one of the common implementations, including, for example, the 15 000 to 20 000 lines of the BSD implementation—optimized and multithreaded C code, time dependent, with asynchronous event handlers, intertwined with the operating system, and security critical. This article reports on work done in the Netsem project to develop lightweight mathematically rigorous techniques that can be applied to such systems: to specify their behavior precisely (but loosely enough to permit the required implementation variation) and to test whether these specifications and the implementations correspond with specifications that are executable as test oracles. We developed post hoc specifications of TCP, UDP, and the Sockets API, both of the service that they provide to applications (in terms of TCP bidirectional stream connections) and of the internal operation of the protocol (in terms of TCP segments and UDP datagrams), together with a testable abstraction function relating the two. These specifications are rigorous, detailed, readable, with broad coverage, and rather accurate. Working within a general-purpose proof assistant (HOL4), we developed language idioms (within higher-order logic) in which to write the specifications: operational semantics with nondeterminism, time, system calls, monadic relational programming, and so forth. We followed an experimental semantics approach, validating the specifications against several thousand traces captured from three implementations (FreeBSD, Linux, and WinXP). Many differences between these were identified, as were a number of bugs. Validation was done using a special-purpose symbolic model checker programmed above HOL4. Having demonstrated that our logic-based engineering techniques suffice for handling real-world protocols, we argue that similar techniques could be applied to future critical software infrastructure at design time, leading to cleaner designs and (via specification-based testing) more robust and predictable implementations. In cases where specification looseness can be controlled, this should be possible with lightweight techniques, without the need for a general-purpose proof assistant, at relatively little cost. [ABSTRACT FROM AUTHOR]

Published
2019
Full Text
View/download PDF

16. Gas pipeline hack adds to America's vulnerabilities

Author

Daschle, Tom and Ridge, Tom

Subjects
Colonial Pipeline Co. -- Safety and security measures -- Crimes against, Bioterrorism -- Forecasts and trends, Petroleum services industry -- Safety and security measures -- Crimes against, Cyberterrorism -- Cases -- Forecasts and trends, Gas pipelines -- Safety and security measures -- Crimes against, Company legal issue, Market trend/market analysis, News, opinion and commentary
Abstract

Byline: Tom Daschle and Tom Ridge, Bipartisan Commission on Biodefense The effects of the ransomware attack that shut down the Colonial Pipeline and disrupted East Coast gasoline supplies have eased. [...]

Published
2021

18. We cannot afford one more day without a confirmed DHS leader

Author

Chertoff, Michael, Johnson, Jeh, Napolitano, Janet, and Ridge, Tom

Subjects
United States. Department of Homeland Security -- Powers and duties -- Officials and employees, General interest, News, opinion and commentary
Abstract

Byline: Michael Chertoff, Jeh Johnson, Janet Napolitano and Tom Ridge For Print Use Only. We urge the Senate to promptly consider and confirm Alejandro Mayorkas, President-elect Joe Biden's nominee for [...]

Published
2021

21. Trust our elections: former DHS chiefs

Author

Chertoff, MIchael, Johnson, Jeh, Napolitano, Janet, and Ridge, Tom

Subjects
United States. Department of Homeland Security -- Officials and employees, Voting -- Social aspects, Elections -- Social aspects, Nonprofit organizations -- Aims and objectives -- Planning, Company business planning, News, opinion and commentary
Abstract

Byline: Michael Chertoff, Jeh Johnson,, Janet Napolitano and Tom Ridge American democracy is based on the premise that we the people create a government that operates only by the consent [...]

Published
2020

22. Armed protesters dishonor veterans

Author

Ridge, Tom

Subjects
Activists -- Evaluation -- Beliefs, opinions and attitudes, Epidemics -- Economic aspects -- United States, Veterans -- Beliefs, opinions and attitudes, COVID-19 -- Economic aspects -- Demonstrations and protests, Infection control -- Demonstrations and protests -- Economic aspects, Americans, Coronaviruses, Coronavirus infections, Military decorations, News, opinion and commentary
Abstract

Byline: Tom Ridge Bennie Adkins died the other day. The retired Army command sergeant major was 86 and had fought a 23-day battle against coronavirus. A little more than 50 [...]

Published
2020

26. Engineering with Logic

Author

Bishop, Steve, primary, Fairbairn, Matthew, additional, Mehnert, Hannes, additional, Norrish, Michael, additional, Ridge, Tom, additional, Sewell, Peter, additional, Smith, Michael, additional, and Wansbrough, Keith, additional

Published
2018
Full Text
View/download PDF

27. CLOSING LOOPHOLE IN FIGHT AGAINST OPIOIDS

Author

Ridge, Tom

Subjects
Opioid abuse, Opioids, General interest, News, opinion and commentary
Abstract

Byline: Tom Ridge, Special to North Jersey Record New Jersey Attorney General Gurbir Grewal announced a new executive office tasked with fighting opioid addiction this spring. But in the same [...]

Published
2018

28. Visualizing the Evaluation of Functional Programs for Debugging

Author

Whitington, John and Ridge, Tom

Subjects
000 Computer science, knowledge, general works, Computer Science
Abstract

In this position paper, we present a prototype of a visualizer for functional programs. Such programs, whose evaluation model is the reduction of an expression to a value through repeated application of rewriting rules, and which tend to make little or no use of mutable state, are amenable to visualization in the same fashion as simple mathematical expressions, with which every schoolchild is familiar. We show how such visualizations may be produced for the strict functional language OCaml, by direct interpretation of the abstract syntax tree and appropriate pretty-printing. We describe (and begin to address) the challenges of presenting such program traces in limited space and of identifying their essential elements, so that our methods will one day be practical for more than toy programs. We consider the problems posed by the parts of modern functional programming which are not purely functional such as mutable state, input/output and exceptions. We describe initial work on the use of such visualizations to address the problem of program debugging, which is our ultimate aim.

Published
2017
Full Text
View/download PDF

30. Visualizing the Evaluation of Functional Programs for Debugging

Author

John Whitington and Tom Ridge, Whitington, John, Ridge, Tom, John Whitington and Tom Ridge, Whitington, John, and Ridge, Tom

Abstract

In this position paper, we present a prototype of a visualizer for functional programs. Such programs, whose evaluation model is the reduction of an expression to a value through repeated application of rewriting rules, and which tend to make little or no use of mutable state, are amenable to visualization in the same fashion as simple mathematical expressions, with which every schoolchild is familiar. We show how such visualizations may be produced for the strict functional language OCaml, by direct interpretation of the abstract syntax tree and appropriate pretty-printing. We describe (and begin to address) the challenges of presenting such program traces in limited space and of identifying their essential elements, so that our methods will one day be practical for more than toy programs. We consider the problems posed by the parts of modern functional programming which are not purely functional such as mutable state, input/output and exceptions. We describe initial work on the use of such visualizations to address the problem of program debugging, which is our ultimate aim.

Published
2017
Full Text
View/download PDF

31. Fighting Terrorism.

Author

Ridge, Tom

Subjects
*PUBLIC officers, *NATIONAL security, *TSUNAMIS
Abstract

Presents a speech by Tom Ridge, secretary of the U. S. Department of Homeland Security, delivered at the London School of Economics in England on January 14, 2005. Discussion on the need for global response against terrorism; Impact of the tsunami disaster on humanity; Views on the international implications of homeland security.

Published
2005

32. Never Any Doubt: A Resilient America

Author

Ridge, Tom

Abstract

This article appeared in Homeland Security Affairs (September 2011), v.7 no.2 "Former DHS Secretary Tom Ridge reminds us of the dangers of complacency and that 'ten years is enough time to know that in the next ten years, the fight will still be with us.' He also reminds us that as new threats surface our tools, policies and security strategies must continue to evolve. 'Because after taking fifty years to win the Cold War, while we emerged as the lone superpower, we were also left with a stockpile of weapons, tactics, and diplomatic relationships that were of little utility in the new security environment.'" Approved for public release; distribution is unlimited.

Published
2011

33. The 1st Verified Software Competition, Extended Experience Report

Author

Muller, Peter, Shankar, Natarajan, Leavens, Gary T., Ridge, Tom, Tuerk, Thomas, Klebanov, Vladimir, Ulbrich, Mattias, Weisse, Benjamin, Leino, K. Rustan M., Chapman, Rod, Monahan, Rosemary, Polikarpova, Nadia, Bronish, Derek, Arthan, Rob, Alkassar, Eyad, Cohen, Ernie, Hillebrand, Mark, Tobies, Stephan, Jacobs, Bart, Piessens, Frank, and Smans, Jan

Subjects
Computer Science
Abstract

We, the organizers and participants, report our experiences from the 1st Veried Software Competition, held in August 2010 in Edinburgh at the VSTTE 2010 conference

Published
2011

34. SibylFS

Author

Ridge, Tom, primary, Sheets, David, additional, Tuerk, Thomas, additional, Giugliano, Andrea, additional, Madhavapeddy, Anil, additional, and Sewell, Peter, additional

Published
2015
Full Text
View/download PDF

37. Lem

Author

Mulligan, Dominic P., primary, Owens, Scott, additional, Gray, Kathryn E., additional, Ridge, Tom, additional, and Sewell, Peter, additional

Published
2014
Full Text
View/download PDF

38. Mr. President, stand up for Simpson-Bowles

Author

Ridge, Tom and Davis, Lanny

Subjects
Public debts -- Political aspects, Economic policy -- Political aspects, News, opinion and commentary
Abstract

Byline: Tom Ridge and Lanny Davis We have heard the president and leaders of both parties talk about the need for a 'balanced approach' in addressing our nation's unsustainable and [...]

Published
2013

39. 'A Single Mission'.

Author

Ridge, Tom

Subjects
*WEAPONS of mass destruction, *NUCLEAR energy
Abstract

Analyzes the concept and objectives of Department of Homeland Security in the U.S. Protection of borders, airports and seaports; Assessment of threats from weapons of mass destruction; Regulation in the distribution of potassium iodine use for nuclear power facility.

Published
2002

40. The methanol alternative to gasoline

Author

Ridge, Tom and Peters, Mary E.

Subjects
Transportation equipment industry -- Economic aspects, Methanol -- Prices and rates, Natural gas -- Economic aspects, Gas industry -- Economic aspects, Company pricing policy, General interest, News, opinion and commentary
Abstract

PRESIDENT Obama recently called the United States the ''Saudi Arabia of natural gas'' and asserted that it was time for our oil-dominated transportation fuel market to open the door to [...]

Published
2012

41. US must play role in world

Author

Ridge, Tom and Shalala, Donna

Subjects
United States -- International relations, Foreign policy, Diplomacy, Political science
Abstract

* It is always difficult to maintain our investments and commitments in times of economic difficulty and rising debt. But from our times in Washington, we know the alternative of [...]

Published
2012

42. How to beat gambling Al Capones

Author

Freeh, Louis and Ridge, Tom

Subjects
Online gambling -- Laws, regulations and rules -- Control, Consumer protection -- Laws, regulations and rules, Law enforcement -- Methods, Government regulation, Sports/gambling game, Political science, Unlawful Internet Gambling Enforcement Act of 2006
Abstract

Al Capone famously said that Prohibition caused nothing but trouble. Although he himself caused much of it, he did have a point. The Volstead Act, which banned alcohol, was well-intentioned [...]

Published
2011

43. We need a terror court

Author

Ridge, Tom

Subjects
Terrorists -- Cases, Court administration -- Evaluation, Justice, Administration of -- Methods -- United States, Company legal issue, News, opinion and commentary
Abstract

Byline: Tom Ridge The arrest of Faisal Shahzad, the man accused of driving a car bomb into Times Square, has generated a lot of high-fives from both the public and [...]

Published
2010

44. The Semantics of x86-CC Multiprocessor Machine Code

Author

Sarkar, Susmit, Sewell, Peter, Zappa Nardelli, Francesco, Owens, Scott, Ridge, Tom, Braibant, Thomas, Myreen, Magnus O., Alglave, Jade, Sarkar, Susmit, Sewell, Peter, Zappa Nardelli, Francesco, Owens, Scott, Ridge, Tom, Braibant, Thomas, Myreen, Magnus O., and Alglave, Jade

Abstract

Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion. We develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanised in HOL. We test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. For programs that are (in some precise sense) data-race free, we prove in HOL that their behaviour is sequentially consistent. We also contrast the x86 model with some aspects of Power and ARM behaviour. This provides a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code.

Published
2009

45. Lem.

Author

Mulligan, Dominic P., Owens, Scott, Gray, Kathryn E., Ridge, Tom, and Sewell, Peter

Published
2014
Full Text
View/download PDF

48. Needed: a G.O.P. Environmental Identity

Author

Ridge, Tom

Subjects
Roosevelt, Theodore -- Political activity
Abstract

At the turn of the century, President Theodore Roosevelt derided political leaders who talked a good game on the environment but did little else as 'nature fakers.' Roosevelt would probably […]

Published
1999

49. Operational Reasoning for Concurrent Caml Programs and Weak Memory Models.

Author

Hutchison, David, Kanade, Takeo, Kittler, Josef, Kleinberg, Jon M., Mattern, Friedemann, Mitchell, John C., Naor, Moni, Nierstrasz, Oscar, Pandu Rangan, C., Steffen, Bernhard, Sudan, Madhu, Terzopoulos, Demetri, Tygar, Doug, Vardi, Moshe Y., Weikum, Gerhard, Schneider, Klaus, Brandt, Jens, and Ridge, Tom

Abstract

This paper concerns the formal semantics of programming languages, and the specification and verification of software. We are interested in the verification of real programs, written in real programming languages, running on machines with real memory models. To this end, we verify a Caml implementation of a concurrent algorithm, Peterson's mutual exclusion algorithm, down to the operational semantics. The implementation makes use of Caml features such as higher order parameters, state, concurrency and nested general recursion. Our Caml model includes a datatype of expressions, and a small step reduction relation for programs (a Caml expression together with a store). We also develop a new proof of correctness for a modified version of Peterson's algorithm, designed to run on a machine with a weak memory. [ABSTRACT FROM AUTHOR]

Published
2007
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results