Secure Synthesis of Code: A Process Improvement Experiment

No abstract is available for this paper.

• Publication year

  1999

• Venue

  World Congress on Formal Methods

• Publication date

  1999-09-20

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/3-540-48118-4_46
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• SOFTWARE CONSIDERATIONS IN AIRBORNE SYSTEMS AND EQUIPMENT CERTIFICATION

  2001cited by this paper
• A case study in innovative process improvement: code synthesis from formal specifications

  1999cited by this paper
• Experiences Using Lightweight Formal Methods for Requirements Modeling

  1998cited by this paper
• Isabelle: A Generic Theorem Prover

  1994cited by this paper
• Targeting safety-related errors during software requirements analysis

  1993cited by this paper
• Integration of Formal Methods with System Design

  1991cited by this paper
• Definition of standard ML

  1990cited by this paper
• Formal system design

  1989cited by this paper
• Formal Methods Applied to a Floating-Point Number System

  1989cited by this paper
• The Formal Verification of Safety-critical Assembly Code

  1988cited by this paper

• Where are we now, and where do we go from here?

  2019cites this paper
• Extending Operation Semantics to Enhance the Applicability of Formal Refinement

  2014cites this paper
• Rewriting Logic and Its Applications

  2014cites this paper
• Foundations for Ensemble Modeling - The Helena Approach - Handling Massively Distributed Systems with ELaborate ENsemble Architectures

  2014cites this paper
• Formalization of Mobile UML Statechart Diagrams Using the π-calculus: An Approach for Modeling and Analysis

  2014cites this paper
• Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

  2014cites this paper
• Formal System Modelling Using Abstract Data Types in Event-B

  2014cites this paper
• Quiescent Consistency: Defining and Verifying Relaxed Linearizability

  2014cites this paper
• Dependability and Safety Analysis of ETCS Communication for ERTMS Level 3 Using Performance Statecharts and Analytic Estimation

  2014cites this paper
• Logic Foundations of the OCL Modelling Language

  2014cites this paper
• Everlasting Challenges with the OBJ Language Family

  2014cites this paper
• Synthesis of Infinite-State Abstractions and Their Use for Software Validation

  2014cites this paper
• Data-Flow Based Model Analysis and Its Applications

  2013cites this paper
• GOAL for Games, Omega-Automata, and Logics

  2013cites this paper
• Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking

  2013cites this paper
• Compositional Approach to Suspension and Other Improvements to LTL Translation

  2013cites this paper
• Three SCC-Based Emptiness Checks for Generalized Büchi Automata

  2013cites this paper
• A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper

  2013cites this paper
• Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems

  2013cites this paper
• The Modelling Framework: Event-B

  2013cites this paper
• Evaluating Human-Human Communication Protocols with Miscommunication Generation and Model Checking

  2013cites this paper
• Model Checking Using Generalized Testing Automata

  2012cites this paper
• A Generic Cyclic Theorem Prover

  2012cites this paper
• Temporal Monitors for TinyOS

  2012cites this paper
• Discharging Proof Obligations from Atelier B Using Multiple Automated Provers

  2012cites this paper
• Efficient and Trustworthy Tool Qualification for Model-Based Testing Tools

  2012cites this paper
• A Certified Multi-prover Verification Condition Generator

  2012cites this paper
• Hybrid On-the-Fly LTL Model Checking with the Sweep-Line Method

  2012cites this paper
• Improved Multi-Core Nested Depth-First Search

  2012cites this paper
• Verification of Open Concurrent Object Systems

  2012cites this paper
• Unifying Lazy and Strict Computations

  2012cites this paper
• Linking Unlinkability

  2012cites this paper
• Lessons Learnt from the Adoption of Formal Model-Based Development

  2012cites this paper
• An UML Model Query Method Based on Structure Pattern Matching

  2012cites this paper
• On the Relationship between LTL Normal Forms and Büchi Automata

  2012cites this paper
• Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic

  2012cites this paper
• Formal Probabilistic Analysis of Cyber-Physical Transportation Systems

  2012cites this paper
• When Structural Refinement of Components Keeps Temporal Properties over Reconfigurations

  2012cites this paper
• Büchi Store: An Open Repository of Büchi Automata

  2011cites this paper
• Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy

  2011cites this paper
• Biased Model Checking Using Flows

  2011cites this paper
• Integration of Bounded Model Checking and Deductive Verification

  2011cites this paper
• Structured Specifications for Better Verification of Heap-Manipulating Programs

  2011cites this paper
• A Multi-encoding Approach for LTL Symbolic Satisfiability Checking

  2011cites this paper
• Tool Interoperability in the Maude Formal Environment

  2011cites this paper
• A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence

  2010cites this paper
• Team Automata Based Framework for Spatio-Temporal RBAC Model

  2010cites this paper
• Modeling Identity-Related Properties and Their Privacy Strength

  2010cites this paper
• A Refinement Methodology for Object-Oriented Programs

  2010cites this paper
• Complexity of Anonymity for Security Protocols

  2010cites this paper
• Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned

  2010cites this paper
• Context-Enhanced Directed Model Checking

  2010cites this paper
• Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems

  2010cites this paper
• A Calculus for the Analysis of Wireless Network Security Protocols

  2010cites this paper
• A Bibliography of Willem-Paul de Roever

  2010cites this paper
• Fostering Proof Scores in CafeOBJ

  2010cites this paper
• Proof Process Evaluation with Mutation Analysis

  2010cites this paper
• Executable Specification of Cryptofraglets in Maude for Security Verification

  2009cites this paper
• A Lazy Unbounded Model Checker for Event-B

  2009cites this paper
• Formal Verification of Avionics Software Products

  2009cites this paper
• The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection

  2009cites this paper
• The Causal Graph Revisited for Directed Model Checking

  2009cites this paper
• Checking Timed Büchi Automata Emptiness Using LU-Abstractions

  2009cites this paper
• Survey on Directed Model Checking

  2009cites this paper
• Transition-Based Directed Model Checking

  2009cites this paper
• Compositional Verification of Input-Output Conformance via CSP Refinement Checking

  2009cites this paper
• Formalization and Rule-Based Transformation of EMF Ecore-Based Models

  2009cites this paper
• Relaxation Refinement: A New Method to Generate Heuristic Functions

  2009cites this paper
• On-the-fly Emptiness Check of Transition-Based Streett Automata

  2009cites this paper
• Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control a laSpec#

  2009cites this paper
• Dependability analysis of the data communication system in train control system

  2009cites this paper
• Verification, Performance Analysis and Controller Synthesis for Real-Time Systems

  2009cites this paper
• Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction

  2009cites this paper
• Fast and Accurate Bounds on Linear Programs

  2009cites this paper
• A Graph-Based Operational Semantics of OO Programs

  2009cites this paper
• Automated Property Verification for Large Scale B Models

  2009cites this paper
• Compositional Model-Checking Verification of Critical Systems

  2008cites this paper
• Model Based Refinement and the Tools of Tomorrow

  2008cites this paper
• MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs

  2008cites this paper
• Diagnostic Information for Realizability

  2008cites this paper
• Faster Than Uppaal?

  2008cites this paper
• From Model Driven Engineering to Verification Driven Engineering

  2008cites this paper
• Guided Test Generation from CSP Models

  2008cites this paper
• Software Engineering with Formal Methods: Experiences with the Development of a Storm Surge Barrier Control System

  2008cites this paper
• Using Coloured Petri Nets to Model and Verify Telecommunications Systems

  2008cites this paper
• Extending Formal Methods for Software-Intensive Systems

  2008cites this paper
• Direct Support for Model Checking Abstract State Machines by Utilizing Simulation

  2008cites this paper
• New Approach for EFSM-Based Passive Testing of Web Services

  2007cites this paper
• Intuitionistic Refinement Calculus

  2007cites this paper
• Granulation as a Privacy Protection Mechanism

  2007cites this paper
• On Synthesizing Controllers from Bounded-Response Properties

  2007cites this paper
• Lifting General Correctness into Partial Correctness is ok

  2007cites this paper
• Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking

  2007cites this paper
• Testable Requirements and Specifications

  2007cites this paper
• Efficient On-the-Fly Algorithms for Partially Observable Timed Games

  2007cites this paper
• Application of Modified Coloured Petri Nets to Modeling and Verification of SDL Specified Communication Protocols

  2007cites this paper
• An Incremental and Modular Technique for Checking LTL\X Properties of Petri Nets

  2007cites this paper
• Modelling and Proof Analysis of Interrupt Driven Scheduling

  2007cites this paper
• Refinement of eb3 Process Patterns into B Specifications

  2007cites this paper
• Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL

  2007cites this paper