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