Logics of Programs [[electronic resource] ] : Workshop Carnegie Mellon University Pittsburgh, PA, June 6-8, 1983 / / edited by E. Clarke, D. Kozen |
Edizione | [1st ed. 1984.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1984 |
Descrizione fisica | 1 online resource (VI, 531 p.) |
Disciplina | 005.1015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer logic
Mathematical logic Logics and Meanings of Programs Mathematical Logic and Formal Languages |
ISBN | 3-540-38775-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A static analysis of CSP programs -- Compactness in semantics for merge and fair merge -- Algebraic tools for system construction -- PC-compactness, a necessary condition for the existence of sound and complete logics of partial correctness -- The intractability of validity in logic programming and dynamic logic -- A semantics and proof system for communicating processes -- Non-standard fixed points in first order logic -- Automatic verification of asynchronous circuits -- Mathematics as programming -- Characterization of acceptable by algol-like programming languages -- A rigorous approach to fault-tolerant system development -- A sound and relatively complete axiomatization of clarke's language L4 -- Deciding branching time logic: A triple exponential decision procedure for CTL -- Equations in combinatory algebras -- Reasoning about procedures as parameters -- Introducing institutions -- A complete proof rule for strong equifair termination -- Necessary and sufficient conditions for the universality of programming formalisms -- There exist decidable context free propositonal dynamic logics -- A decision procedure for the propositional ?-calculus -- A verifier for compact parallel coordination programs -- Information systems, continuity and realizability -- A complete system of temporal logic for specification schemata -- Reasoning in interval temporal logic -- Hoare's logic for programs with procedures — What has been achieved? -- A theory of probabilistic programs -- A low level language for obtaining decision procedures for classes of temporal logics -- Deriving efficient graph algorithms (summary) -- An introduction to specification logic -- An interval-based temporal logic -- Property preserving homomorphisms of transition systems -- From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview -- Yet another process logic -- A proof system for partial correctness of dynamic networks of processes -- Errata. |
Record Nr. | UNISA-996466341303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1984 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logics of Programs [[electronic resource] ] : Workshop, Yorktown Heights, NY, USA / / edited by D. Kozen |
Edizione | [1st ed. 1982.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 |
Descrizione fisica | 1 online resource (VIII, 429 p.) |
Disciplina | 005.1015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer logic
Logics and Meanings of Programs |
ISBN | 3-540-39047-2 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Proof rules dealing with fairness -- Hoare's Logic is incomplete when it does not have to be -- The refinement of specifications and the stability of Hoare's Logic -- Toward a logical theory of program data -- Design and synthesis of synchronization skeletons using branching time temporal logic -- The type theory of PL/CV3 -- Correctness of programs with function procedures -- A formalism for reasoning about fair termination -- Keeping a foot on the ground -- Further results on propositional dynamic logic of nonregular programs -- Some observations on compositional semantics -- Some connections between iterative programs, recursive programs, and first-order logic -- On induction vs. *-continuity -- Timesets -- Program logics and program verification -- Verification of concurrent programs: Temporal proof principles -- Synthesis of communicating processes from Temporal Logic specifications -- A note on equivalences among logics of programs -- The representation theorem for algorithmic algebras -- Nonstandard Dynamic Logic -- A critique of the foundations of Hoare-style programming logics -- Some applications of topology to program semantics -- Using graphs to understand PDL -- Critical remarks on max model of concurrency -- Transcript of panel discussion. |
Altri titoli varianti | With contributions by nummerous experts |
Record Nr. | UNISA-996466338403316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|