Logics of programs : Workshop, Carnegie Mellon University, Pittsburgh, PA, June 6 8, 1983

Zapisane w:
Opis bibliograficzny
Korporacja: Workshop on logics of programs :Pittsburgh
Kolejni autorzy: Clarke, Edmund M., 1945-2020 (Dyrektor wydawnictwa), Kozen, Dexter C., 1951- (Dyrektor wydawnictwa)
Format: Livre numérique
Język:Anglais
Wydane: Berlin [etc.] : Springer [20..].
Cham : Springer Nature
Seria:Lecture notes in computer science 164
Hasła przedmiotowe:
Dostęp online:Accès sur la plateforme de l'éditeur
Accès sur la plateforme Istex
Accès Université d'Orléans
Accès INSA CVL
Komentarz: Archives Springer e-books (Licence nationale)
Archives Springer e-books (Licence nationale)
Autres localisations: Voir dans le Sudoc
Edition sous un autre format:• Logics of programs, Workshop, Carnegie-Mellon University, Pittsburgh, PA, June 6-8, 1983, ed. by Edmund Clarke and Dexter Kozen, Berlin, Springer, 1984, 1 vol. (VI-528 p.), Lecture notes in computer science, 3-540-12896-4
• Logics of Programs, Texte imprimé, 9783662172384
Spis treści:
  • 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 semanticsfor ALGOL-like languages: An overview
  • Yet another process logic
  • A proof system for partial correctness of dynamic networks of processes
  • Errata.