Proof of correctness of data representations
From MaRDI portal
Cites work
Cited in
(only showing first 100 items - show all)- A view of computability on term algebras
- Non-deterministic data types: Models and implementations
- Pushdown machines for the macro tree transducer
- Crypt-equivalent algebraic specifications
- Proving entailment between conceptual state specifications
- Algebraic specifications of computable and semicomputable data types
- Equational specification of partial higher-order algebras
- Semantics and verification of monitors and systems of monitors and processes
- Auxiliary variables in data refinement
- Correctness proofs for abstract implementations
- Final algebra semantics and data type extensions
- An approach for data type specification and its use in program verification
- Hierarchical program specification and verification - a many-sorted logical approach
- Invariants in the application-oriented specification of control systems
- Specifications, models, and implementations of data abstractions
- Data refinement of predicate transformers
- Iterated stack automata and complexity classes
- Language design methods based on semantic principles
- On a new approach to representation independent data classes
- Proving programs correct through refinement
- The correctness of the Schorr-Waite list marking algorithm
- Program refinement in fair transition systems
- The lattice of data refinement
- Software perfective maintenance: Including retrainable software in software reuse
- Essential concepts of algebraic specification and program development
- Proof systems for structured specifications with observability operators
- Swinging types=functions+relations+transition systems
- A hidden agenda
- A logic for the stepwise development of reactive systems
- The verification and synthesis of data structures
- Objects and classes in Algol-like languages
- Secure implementation of channel abstractions
- Observational logic, constructor-based logic, and their duality.
- Applying abstraction and formal specification in numerical software design
- Data refinement, call by value and higher order programs
- Lax naturality through enrichment
- Stepwise refinement of heap-manipulating code in Chalice
- Calculating with acyclic and cyclic lists
- Principal abstract families of weighted tree languages
- Abstract implementation of algebraic specifications in a temporal logic language
- Extended transitive separation logic
- Constructor-based observational logic
- Automatic refinement to efficient data structures: a comparison of two approaches
- Preservation of probabilistic information flow under refinement
- On assertion-based encapsulation for object invariants and simulations
- Specification and verification challenges for sequential object-oriented programs
- The refinement calculus of reactive systems
- A coalgebraic semantics of subtyping
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Automatic functional correctness proofs for functional search trees
- Syntactic logical relations for polymorphic and recursive types
- A framework for establishing formal conformance between object models and object-oriented programs
- Invariants for non-hierarchical object structures
- Work it, wrap it, fix it, fold it
- Building a Modal Interface Theory for Concurrency and Data
- Transitive Separation Logic
- Data refinement of invariant based programs
- Partiality, state and dependent types
- Dynamic frames in Java dynamic logic
- Factorising folds for faster functions
- WP semantics and behavioral subtyping
- Dynamic logic with binders and its application to the development of reactive systems
- Types in programming languages, between modelling, abstraction, and correctness (extended abstract)
- Approximation of weighted automata with storage
- An Introduction to Grammar Convergence
- The worker/wrapper transformation
- Iterated linear control and iterated one-turn pushdowns
- On the design and specification of message oriented programs
- Object-oriented programming: some history, and challenges for the next fifty years
- Recursive data structures
- Program specification and data refinement in type theory
- Invariant diagrams with data refinement
- Certifying algorithms
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- Modular specification of frame properties in JML
- Algebraic implementation of abstract data types: a survey of concepts and new compositionality results
- Category theoretic models of data refinement
- Axiomatics for data refinement in call by value programming languages
- A technique for specifying and refining TCSP processes by using guards and liveness conditions
- Constructing systems as object communities
- Proving the correctness of behavioural implementations
- A decade of TAPSOFT. Aspects of progress and prospects in theory and practice of software development
- Loop invariants: analysis, classification, and examples
- Interfaces between languages for communicating systems
- Observational interpretation of Casl specifications
- Interface theories for concurrency and data
- Computing with locally effective matrices
- Retrenchment and refinement interworking: the tower theorems
- Prespecification in data refinement
- Strict linearizability and abstract atomicity
- Sound and relaxed behavioural inheritance
- Behavioural satisfaction and equivalence in concrete model categories
- Refinement and state machine abstraction
- Blaming the client: on data refinement in the presence of pointers
- Abstraction for concurrent objects
- Algebraic proofs of consistency and completeness
- On the correctness of modular systems
- Dependent type refinements for futures
- A single complete rule for data refinement
- Compositional refinement of interactive systems modelled by relations
This page was built for publication: Proof of correctness of data representations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2554952)
