Tom Maibaum

About

From Wikipedia

Thomas Stephen Edward Maibaum Fellow of the Royal Society of Arts is a computer scientist.Maibaum has a Bachelor of Science undergraduate degree in pure mathematics from the University of Toronto, Canada , and a Doctor of Philosophy in computer science from Queen Mary and Royal Holloway Colleges, University of London, England .

Published Works

• Categorical semantics of parallel program design
• Sharing actions and attributes in modal action logic
• A generalized approach to formal languages
• On a generalized modularization theorem
• Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving
• The prescription and description of state based systems
• Deontic action logic, atomic boolean algebras and fault-tolerance
• Intermodeling, Queries, and Kleisli Categories
• Software Certification: Is There a Case against Safety Cases?
• Sometimes “Tomorrow” is “Sometime”
Interconnecting formalisms
A theory of abstract data types for program development: Bridging the gap?
Objects, associations and subsystems: A hierarchical approach to encapsulation
Evaluating the Effectiveness of a Goal-Oriented Requirements Engineering Method
A Complete and Compact Propositional Deontic Logic
Higher order data types
On the Modularization Theorem for logical specifications
Towards specification, modelling and analysis of fault tolerance in self managed systems
A model management approach for assurance case reuse due to system evolution
Mathematical foundations of software engineering
Conservative extensions, interpretations between theories and all that!
Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting
Can Product-Specific Assurance Case Templates Be Used as Medical Device Standards?
Reasoning about static and dynamic properties in alloy
Category Theory and Model-Driven Engineering: From Formal Semantics to Design Patterns and Beyond
Mapping-Aware Megamodeling: Design Patterns and Laws
A Constructive Presentation for the Modal Connective of Necessity (□)
Safety cases: A review of challenges
A Tableaux System for Deontic Action Logic
Formally specifying temporal constraints and error recovery
Continuous Data Types
Model management for regulatory compliance
Towards a Verification Logic for Rewriting Logic
An Event-B Approach to Timing Issues Applied to the Generic Insulin Infusion Pump
A pluralistic knowledge-based approach to software specification
Synthesising Interconnections
Generalising Interpretations Between Theories in the Context of (π-)institutions
Pumping lemmas for term languages
Hierarchical Temporal Specifications of Dynamically Reconfigurable Component Based Systems
A rely–guarantee discipline for open distributed systems design
Software certification experience in the canadian nuclear industry
The Epistemology of Validation and Verification Testing
Logical specification and implementation
Towards a Compositional Interpretation of Object Diagrams
Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications
Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows
Axiomatising Specification Theory
A Software Certification Consortium and its Top 9 Hurdles
Implementability of requirements in the four-variable model
A Verification Logic for Rewriting Logic
FDA: Between Process and Product Evaluation
Compositional Structuring in the B-Method: A Logical Viewpoint of the Static Context
Process semantics of temporal logic specification
Formalizing the Glucose Homeostasis Mechanism
On Software Certification: We Need Product-Focused Approaches
Characterizing Fault-Tolerant Systems by Means of Simulation Relations
Conceptual modeling of data base operations
Database Instances, Abstract Data Types and Database Specification
The very idea of software development environments: a conceptual architecture for the arts' environment paradigm
The Definition and Assessment of a Safety Argument
The characterisation of the derivation trees of context free sets of terms as regular sets
Proof theory and computer programming
A communication data type for message oriented programming
Interpretability of First—Order Dynamic Logic in a Relational Calculus
A Logical Basis for the Specification of Reconfigurable Component-Based Systems
Towards Dynamic Population Management of Abstract Machines in the B Method
Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic
The Semantics of Cardinality-Based Feature Models via Formal Languages
Modeling Product Lines with Kripke Structures and Modal Logic
Safety Case Impact Assessment in Automotive Software Systems: An Improved Model-Based Approach
Use of Tabular Expressions for Refinement Automation
The GOPCSD Tool: An Integrated Development Environment for Process Control Requirements and Design
A Categorical Approach to Structuring and Promoting Z Specifications
Deontic Logic, Contrary to Duty Reasoning and Fault Tolerance
Erratum
Notes on refinement, interpolation and uniformity
Taking a page from the law books: Considering evidence weight in evaluating assurance case confidence
Interconnecting formalisms
What we teach software engineers in the university
Assurance via model transformations and their hierarchical refinement
Abstract Data Types and Type Theory: Theories as Types
Large database specifications from small views
A Logic for Real-Time Systems Specification Its Algebraic Semantics and Equational Calculus
Equations Compared with Clauses for Specification of Abstract Data Types
Combining Static and Dynamic Impact Analysis for Large-Scale Enterprise Systems
Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements
What Is a Derived Signature Morphism?
Toward Product Lines of Mathematical Models for Software Model Management
Taking Alloy to the Movies
Verifying Temporal Properties of CommUnity Designs
Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy
Large-Scale Enterprise Systems: Changes and Impacts
Categorical foundations for structured specifications in $${\mathsf{Z}}$$ Z
Argument Evaluation in the Context of Assurance Case Confidence Modeling
A test framework for integration testing of object-oriented programs
Stateflow to Tabular Expressions
Extension Morphisms for CommUnity
A top-down step-wise refinement methodology for protocol specification
Separating Safety and Control Systems to Reduce Complexity
On the Construction of Engineering Handbooks
What IS a BoK? Large – Extended Abstract –
Formalizing the Cardiac Pacemaker Resynchronization Therapy
A Model Management Imperative: Being Graphical Is Not Sufficient, You Have to Be Categorical
A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules
Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge
A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case
Requirements-Reuse Using GOPCSD: Component-Based Development of Process Control Systems
Implementing Dynamic Aggregations of Abstract Machines in the B Method
Challenges in Software Certification
Reasoning about System-Degradation and Fault-Recovery with Deontic Logic
Specifying and Verifying Business Processes Using PPML
Characterizing Locality (Encapsulation) with Bisimulation
Towards a First-Order Deontic Action Logic
syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
Simulation relations for fault-tolerance
On what exactly goes on when software is developed step-by-step, II: The sequel
A Branching Time Logical System for Open Distributed Systems Development
Towards a software engineered road for developing process control systems
An ought-to-do deontic logic for reasoning about fault-tolerance: the diarrheic philosophers
Hierarchical Multiset Theories of Cardinality-Based Feature Diagrams
Formal methods versus engineering
A formal approach to rigorous development of critical systems
Towards Dynamically Communicating Abstract Machines in the B Method
Systematising Reactive System Design
Formalising Object-Oriented Models in the Object Calculus
A Framework for Describing Software Architectures for Reuse
Introduction and Motivation
Related Work
A General Method for Composing an Engineering HB
Application of the General Method to the Railway Domain
Example HB Entry of a Formal Method for the Railway Domain — Step 6
Conclusions and Prospects for Future Work
A Separation Principle for Embedded System Interfacing
Is Current Incremental Safety Assurance Sound?
Some Institutional Requirements for Temporal Reasoning on Dynamic Reconfiguration of Component Based Systems
In Memoriam Armando Martín Haeberer
Design in CommUnity with Extension Morphisms
Erratum to: Challenges in Software Certification
Certification of Software-Driven Medical Devices
Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics
A Methodology for Message Oriented Programming
Parallel Rewriting Systems on Terms
Impact Analysis via Reachability and Alias Analysis
Towards Making Safety Case Arguments Explicit, Precise, and Well Founded
On the design and specification of message oriented programs
Message oriented programming—A resource based methodology
A uniform logical treatment of queries and updates, tech. rep. DB018001-1980
A theoretical framework for cardinality-based feature models: The semantics and computational aspects
Encapsulating deontic and branching time specifications
Formal Methods: A Commentary
Editorial
Architecture Based Development with DYNACOMM: Incorporating Dynamic Reconfiguration and Hierarchical Design into CommUnity
Consistency checking of clinical practice guidelines with MITDL
Temporal Specifications of Component Based Systems with Polymorphic Dynamic Reconfiguration
Software certification consortium
Formal Methods: A Commentary
Satisfiability Calculus: An Abstract Formulation of Semantic Proof Systems
Fixed-dose Strategy Is Lacking
Open Questions
Equivalent Treatment Options
Suffers From Conflicts of Interest
Automated Reasoning over Deontic Action Logics with Finite Vocabularies
Actions and Events in Concurrent Systems Design
Faithful Modeling of Product Lines with Kripke Structures and Modal Logic
More Less

Other Resources

• en.wikipedia.org

Schools

Imperial College London

Public research university located in London, United Kingdom

View profile

University of Toronto

University in Toronto, Ontario, Canada

View profile

McMaster University

Public research university in Hamilton, Ontario, Canada

View profile

Influence Rankings by Discipline