Roadmap for enhanced languages and methods to aid verification

No abstract is available for this paper.

• Publication year

  2006

• Venue

  International Conference on Generative Programming: Concepts and Experiences

• Publication date

  2006-10-22

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1173706.1173740
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A simple approach to specifying concurrent systems

  2016cited by this paper
• Towards Verifying Model Transformations

  2008cited by this paper
• Program slicing

  2008cited by this paper
• Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B

  2007cited by this paper
• Multilevel models in model-driven engineering, product lines, and metaprogramming

  2006cited by this paper
• Adding native specifications to JML

  2006cited by this paper
• Autolocker: synchronization inference for atomic sections

  2006cited by this paper
• Modular invariants for layered object structures

  2006cited by this paper
• A theory of object oriented refinement

  2006cited by this paper
• Reasoning About Method Calls in Interface Specifications

  2006cited by this paper
• WHAT IS A PROOF

  2005cited by this paper
• Mechanized Metatheory for the Masses: The PoplMark Challenge

  2005cited by this paper
• Reasoning About Method Calls in JML Specifications

  2005cited by this paper
• Combining programming with theorem proving

  2005cited by this paper
• Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project

  2005cited by this paper
• Simple and Effective Static Analysis to Find Bugs

  2005influential reference
• Extending JML for Modular Specification and Verification of Multi-threaded Programs

  2005cited by this paper
• A language-based approach to functionally correct imperative programming

  2005cited by this paper
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)

  2005cited by this paper
• A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets

  2005cited by this paper
• Digital equipment corporation.

  2004cited by this paper
• Program comprehension in generative programming: a history of grand challenges

  2004cited by this paper
• Object Invariants in Dynamic Contexts

  2004cited by this paper
• The Spec# Programming System: An Overview

  2004cited by this paper
• CASL User Manual

  2004cited by this paper
• Righting Software

  2004cited by this paper
• Declaring and checking non-null types in an object-oriented language

  2003influential reference
• Modular specification of frame properties in JML

  2003cited by this paper
• Facilitating program verification with dependent types

  2003cited by this paper
• Planware II : Synthesis of Schedulers for Complex Resource Systems

  2003cited by this paper
• The verifying compiler: A grand challenge for computing research

  2003cited by this paper
• How the design of JML accommodates both runtime assertion checking and formal verification

  2003cited by this paper
• High Integrity Software - The SPARK Approach to Safety and Security

  2003cited by this paper
• Modular Verification of Performance Constraints

  2003cited by this paper
• Verification of Object-Oriented Programs with Invariants

  2003cited by this paper
• Determining the Specification of a Control System from That of Its Environment

  2003cited by this paper
• Scaling step-wise refinement

  2003cited by this paper
• An overview of JML tools and applications

  2003cited by this paper
• What can we Gain by Integrating a Language Processor with a Theorem Prover

  2003cited by this paper
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002cited by this paper
• Growing the UML

  2002cited by this paper
• On the Use of Data Refinement in the Development of Secure Communications Systems

  2002cited by this paper
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002influential reference
• Modular Specification and Verification of Object-Oriented Programs

  2002cited by this paper
• Model-Driven Approaches to Software Development

  2002cited by this paper
• The SLAM project: debugging system software via static analysis

  2002cited by this paper
• Consolidated Ada Reference Manual Language and Standard Libraries

  2002cited by this paper
• An Overview of AspectJ

  2001influential reference
• Houdini, an Annotation Assistant for ESC/Java

  2001cited by this paper
• Modular Specification of Frame Properties

  2001cited by this paper
• The LOOP Compiler for Java and JML

  2001cited by this paper
• A formal approach to component-based software engineering: education and evaluation

  2001cited by this paper
• Algebraic specification of abstract data types

  2001cited by this paper
• Performance specification of software components

  2001cited by this paper
• Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java

  2001cited by this paper
• TVLA: A System for Implementing Static Analyses

  2000cited by this paper
• Generating Data Analysis Programs from Statistical Models

  2000cited by this paper
• An Electronic Purse: Specification, Refinement and Proof

  2000cited by this paper
• A certifying compiler for Java

  2000cited by this paper
• Generative Programming: Methods, Tools, and Applications

  2000cited by this paper
• Checking system rules using system-specific, programmer-written compiler extensions

  2000influential reference
• Bandera: extracting finite-state models from Java source code

  2000cited by this paper
• Performance specifications of software components

  2000cited by this paper
• Requirements engineering in the year 00: a research perspective

  2000cited by this paper
• Form and content: dissociating syntax and semantics in sentence comprehension.

  1999cited by this paper
• Parametric shape analysis via 3-valued logic

  1999cited by this paper
• Mujava: embedding a programming language in a theorem prover

  1999cited by this paper
• From system F to typed assembly language

  1999cited by this paper
• Principles of Program Analysis

  1999cited by this paper
• Dynamically discovering likely program invariants to support program evolution

  1999cited by this paper
• The object constraint language: precise modeling with UML

  1998cited by this paper
• Flexible Alias Protection

  1998cited by this paper
• Refinement Calculus

  1998cited by this paper
• Extended static checking

  1998cited by this paper
• Reasoning about Java classes: preliminary report

  1998cited by this paper
• Cayenne—a language with dependent types

  1998cited by this paper
• Formalization of Time and Space

  1998cited by this paper
• Compositionality : the significant difference : international symposium, COMPOS '97, Bad Malente, Germany, September 8-12, 1997 : revised lectures

  1998cited by this paper
• Refinement Calculus: A Systematic Introduction

  1998cited by this paper
• Data Refinement: Model-Oriented Proof Methods and their Comparison

  1998cited by this paper
• Revised Lectures from the International Symposium on Compositionality: The Significant Difference

  1997cited by this paper
• Four dark corners of requirements engineering

  1997cited by this paper
• On the Practical Need for Abstraction Relations to Verify Abstract Data Type Representations

  1997cited by this paper
• High Integrity Ada: The Spark Approach

  1997cited by this paper
• Mathematical Notation in Formal Specification: Too Difficult for the Masses?

  1996cited by this paper
• Stepwise Refinement of Communicating Systems

  1996cited by this paper
• Static detection of dynamic memory errors

  1996cited by this paper
• Algebraic semantics of imperative programs

  1996cited by this paper
• Formal methods for industrial applications : specifying and programming the steam boiler control

  1996cited by this paper
• The B-book - assigning programs to meanings

  1996cited by this paper
• Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS

  1995cited by this paper
• An Action System Approach to the Steam Boiler Problem

  1995cited by this paper
• Denotational semantics

  1995cited by this paper
• Ada 95 Reference Manual

  1995cited by this paper
• Part I: the RESOLVE framework and discipline: a research synopsis

  1994cited by this paper
• Part II: specifying components in RESOLVE

  1994cited by this paper
• Deductive Composition of Astronomical Software from Subroutine Libraries

  1994cited by this paper
• On tight performance specification of object-oriented software components

  1994cited by this paper
• Programming from specifications (2nd ed.)

  1994cited by this paper
• The temporal logic of actions

  1994cited by this paper

• A Method to Deduce and Synthesize the Dafny Programs

  2021cites this paper
• University ’ s repository of research publications and other research outputs What can we expect from program verification ? Journal Item

  2020cites this paper
• Contextual Dependency in State-Based Modelling

  2020cites this paper
• Strong functional pearl: Harper’s regular-expression matcher in Cedille

  2020cites this paper
• Modeling and Proving Distributed Algorithms for Dynamic Graphs

  2020cites this paper
• Formal Modeling and Verification of a Distributed Algorithm for Constructing Maximal Cliques in Static Networks

  2019cites this paper
• A Formal Approach for Distributed Computing of Maximal Cliques in Dynamic Networks

  2018cites this paper
• Preuves d'algorithmes distribués par composition et raffinement. (Proofs of Distributed Algorithms by refinement and composition)

  2017cites this paper
• A Formal Approach for Maintaining Forest Topologies in Dynamic Networks

  2017cites this paper
• Proving Distributed Coloring of Forests in Dynamic Networks

  2017cites this paper
• Formal Proof of the Dependable Bypassing Routing Algorithm Suitable for Adaptive Networks on Chip QnoC Architecture

  2017cites this paper
• A correct-by-construction approach for proving distributed algorithms in spanning trees

  2017cites this paper
• Algorithms for Finding Maximal and Maximum Cliques: A Survey

  2017cites this paper
• Applying a Dependency Mechanism for Voting Protocol Models Using Event-B

  2017cites this paper
• Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions

  2016cites this paper
• Towards a General Framework for Ensuring and Reusing Proofs of Termination Detection in Distributed Computing

  2016cites this paper
• On Two Friends for Getting Correct Programs - Automatically Translating Event B Specifications to Recursive Algorithms in Rodin

  2016cites this paper
• A Refinement-Based Approach for Proving Distributed Algorithms on Evolving Graphs

  2016cites this paper
• Deductive Software Verification – The KeY Book

  2016cites this paper
• From Event-B Models to Dafny Code Contracts

  2015cites this paper
• Verification and validation based on the generation of testing sequences from timing diagram specifications in industrial automation

  2015cites this paper
• A formal pattern for dynamic networks through evolving graphs

  2015cites this paper
• Capturing proof process

  2015cites this paper
• Towards a Formal Model for Dynamic Networks Through Refinement and Evolving Graphs

  2015cites this paper
• Enhancing Proofs of Local Computations through Formal Event-B Modularization

  2014cites this paper
• Analysis of Self-⋆ and P2P Systems Using Refinement

  2014cites this paper
• Modelling an Aircraft Landing System in Event-B (Full Report)

  2014cites this paper
• On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems - Version to Read

  2014cites this paper
• Playing with state-based models for designing better algorithms

  2014cites this paper
• Transforming Event B Models into Verified C# Implementations

  2013cites this paper
• Whiley: A Platform for Research in Software Verification

  2013cites this paper
• Formal Specification of Medical Systems by Proof-Based Refinement

  2013cites this paper
• Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms

  2013cites this paper
• From Event-B Specifications to Programs for Distributed Algorithms

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

  2013cites this paper
• Revisiting Snapshot Algorithms by Refinement-Based Techniques

  2012cites this paper
• Research on Automated Sorting Algorithms Generation Based on PAR: Research on Automated Sorting Algorithms Generation Based on PAR

  2012cites this paper
• Formal Verification of Fault Tolerant NoC-based Architecture

  2012cites this paper
• Reliability and Safety of Critical Device Software Systems

  2011cites this paper
• Fiabilité et sûreté des systèmes informatiques critiques

  2011cites this paper
• Investigations in automating software verification

  2011cites this paper
• First-class features

  2011cites this paper
• Medical Protocol Diagnosis Using Formal Methods

  2011cites this paper
• Mechanical and modular verification condition generation for object-based software

  2011cites this paper
• Technical Report on Interpretation of the Electrocardiogram (ECG) Signal using Formal Methods

  2011cites this paper
• Analysis of DSR Protocol in Event-B

  2011cites this paper
• Building a push-button RESOLVE verifier: Progress and challenges

  2011cites this paper
• Technical Report on Formalisation of the Heart using Analysis of Conduction Time and Velocity of the Electrocardiography and Cellular-Automata

  2011cites this paper
• Program Verification and System Dependability

  2010cites this paper
• Seamless Model-Based Development: From Isolated Tools to Integrated Model Engineering Environments

  2010cites this paper
• The Open University ’ s repository of research publications and other research outputs What can we expect from program verification ?

  2010cites this paper
• A four-way framework for validating a specification

  2010cites this paper
• Technical Report on Formal Development of Two-Electrode Cardiac Pacing System

  2010cites this paper
• Event-B Patterns for Specifying Fault-Tolerance in Multi-agent Interaction

  2009cites this paper
• Livrable 3 Proof-based design patterns

  2009cites this paper
• Refinement-Based Guidelines for Algorithmic Systems

  2009cites this paper
• Pacemaker's Functional Behaviors in Event-B

  2009cites this paper
• A simple refinement-based method for constructing algorithms

  2009cites this paper
• Livrable 3 Proof-based design patterns August 6

  2008cites this paper
• A Case Study in Automated Verification

  2008cites this paper
• Reasoning about programs via operational semantics: requirements for a support system

  2008cites this paper
• Workshop on Modularization, Composition, and Generative Techniques for Product Line Engineering

  2008cites this paper
• GRACE TECHNICAL REPORTS Proceedings of the First International Workshop on Formal Methods Education and Training

  2008influential citation
• A Case Study in Automated , Modular , and Full Functional Verification

  2008cites this paper
• Modularizing Theorems for Software Product Lines: The Jbook Case Study

  2008cites this paper
• Towards Reuse with "Feature-Oriented Event-B"

  2008cites this paper
• An incremental process for the development of multi-agent systems in Event-B

  2008cites this paper
• Teaching programming methodology using Event B

  2008cites this paper
• The Composition of Event-B Models

  2008cites this paper
• AFM ’ 08 : Third Workshop on Automated Formal Methods 14 July 2008 Princeton , New Jersey

  2008cites this paper
• Verification and validation of a project collaboration tool

  2008cites this paper
• Using modern mathematics as an FOSD modeling language

  2008cites this paper
• Reflections on, and Predictions for, Support Systems for the Development of Programs

  2008cites this paper
• Editorial (VSTTE Special Issue)

  2007cites this paper
• On The Modularization of Theorems for Software Product Lines

  2007cites this paper
• Towards Semi-Automatic Generation of Provably Correct Algorithmic Programs

  2007cites this paper
• Abstracting Pointers for a Verifying Compiler

  2007cites this paper
• Balancing Insight and Effort: The Industrial Uptake of Formal Methods

  2007cites this paper
• Feature Oriented Model Driven Development: A Case Study for Portlets

  2007cites this paper
• Proved-Patterns-Based Development for Structured Programs

  2007cites this paper
• Feature oriented model driven product lines

  2007cites this paper
• Refinement-based guidelines for developing structured programs

  2007cites this paper
• From implementation to theory in product synthesis

  2007cites this paper
• Team Parsifal Preuves Automatiques et Raisonnement sur des SpécIFicAtions Logiques

  2007cites this paper
• Towards Semi-Automatic Generation of Provably Correct Algorithmic Programs

  2007cites this paper
• On the SYM A evaluation report

  2007cites this paper
• Performance analysis based upon complete profiles

  2006cites this paper
• What Can We Expect from Program Verification?

  2006cites this paper
• Revisiting Snapshot Algorithms by Refinement-based Techniques

  year unknowncites this paper
• RODIN “ Rigorous Open Development Environment for Complex Systems ” RODIN Deliverable D 29 Final report on methodology

  year unknowncites this paper