Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
FME '93: Industrial-Strength Formal Methods [[electronic resource] ] : First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993. Proceedings / / edited by James C.P. Woodcock, Peter G. Larsen
| FME '93: Industrial-Strength Formal Methods [[electronic resource] ] : First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993. Proceedings / / edited by James C.P. Woodcock, Peter G. Larsen |
| Edizione | [1st ed. 1993.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 |
| Descrizione fisica | 1 online resource (XIII, 695 p.) |
| Disciplina | 005.13/1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Application software Computer programming Computer logic Information technology Business—Data processing Software Engineering/Programming and Operating Systems Computer Applications Programming Techniques Software Engineering Logics and Meanings of Programs IT in Business |
| ISBN | 3-540-47623-7 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Reasoning about interference in an object-based design method -- Using relative refinement for fault tolerance -- Specification and validation of a security policy model -- Experiences from applications of RAISE -- Role of VDM(++) in the development of a real-time tracking and tracing system -- The integration of LOTOS with an object oriented development method -- An industrial experience on LOTOS-based prototyping for switching systems design -- Towards an implementation-oriented specification of TP protocol in LOTOS -- A metalanguage for the formal requirement specification of reactive systems -- Model checking in practice -- Algorithm refinement with read and write frames -- Invariants, frames and postconditions: a comparison of the VDM and B notations -- The industrial take-up of formal methods in safety-critical and other areas: A perspective -- A proof environment for concurrent programs -- A VDM ? study of Fault-Tolerant stable storage — Towards a computer engineering mathematics -- Applications of modal logic for the specification of real-time systems -- Formal methods reality check: Industrial usage -- Automating the generation and sequencing of test cases from model-based specifications -- The parallel abstract machine: A common execution model for FDTs -- Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli -- Real-time refinement -- Different FDT's confronted with different ODP-viewpoints of the trader -- On the derivation of executable database programs from formal specifications -- A concurrency case study using RAISE -- Specifying a safety-critical control system in Z -- An overview of the SPRINT method -- Application of composition development method for definition of SYNTHESIS information resource query language semantics -- Verification tools in the development of provably correct compilers -- Encoding W : A Logic for Z in 2OBJ -- Formal verification for fault-tolerant architectures: Some lessons learned -- Conformity clause for VDM-SL -- Process instances in LOTOS simulation -- The SAZ project: Integrating SSADM and Z -- Maintaining consistency under changes to formal specifications -- An EVES data abstraction example -- Putting advanced reachability analysis techniques together: The “ARA” tool -- Integrating SA/RT with LOTOS -- Symbolic model checking for distributed real-time systems -- Adding specification constructors to the refinement calculus -- Selling formal methods to industry -- Tool Descriptions. |
| Record Nr. | UNISA-996466079203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Mathematics of Program Construction [[electronic resource] ] : Second International Conference, Oxford, U.K., June 29 - July 3, 1992. Proceedings / / edited by Richard S. Bird, C.Carroll Morgan, James C.P. Woodcock
| Mathematics of Program Construction [[electronic resource] ] : Second International Conference, Oxford, U.K., June 29 - July 3, 1992. Proceedings / / edited by Richard S. Bird, C.Carroll Morgan, James C.P. Woodcock |
| Edizione | [1st ed. 1993.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 |
| Descrizione fisica | 1 online resource (VIII, 380 p.) |
| Disciplina | 005.1/01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computers Applied mathematics Engineering mathematics Computer programming Algorithms Software Engineering/Programming and Operating Systems Theory of Computation Applications of Mathematics Programming Techniques Software Engineering Algorithm Analysis and Problem Complexity |
| ISBN | 3-540-47613-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extended calculus of constructions as a specification language -- On the economy of doing Mathematics -- Pretty-printing: An exercise in functional programming -- True concurrency: Theory and practice -- Programming for behaviour -- Calculating a path algorithm -- Solving optimisation problems with catamorphisms -- A time-interval calculus -- Conservative fixpoint functions on a graph -- An algebraic construction of predicate transformers -- Upwards and downwards accumulations on trees -- Distributing a class of sequential programs -- (Relational) programming laws in the boom hierarchy of types -- A logarithmic implementation of flexible arrays -- Designing arithmetic circuits by refinement in Ruby -- An operational semantics for the guarded command language -- Shorter paths to graph algorithms -- Logical specifications for functional programs -- Inorder traversal of a binary heap and its inversion in optimal time and space -- A calculus for predicative programming -- Derivation of a parallel matching algorithm -- Modular reasoning in an object-oriented refinement calculus -- An alternative derivation of a binary heap construction function -- A derivation of Huffman's algorithm. |
| Record Nr. | UNISA-996466079803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||