Algebraic Methodology and Software Technology
2004
- Algebraic Approaches to Problem Generalisationby: Roland Carl Backhouse
- Modelling Concurrent Interactionsby: Juliana Küster Filipe
- Formal JVM Code Analysis in JavaFANby: Azadeh Farzan, José Meseguer, Grigore Rosu
- Agent-Oriented Programming: Where Do We Stand?by: John-Jules Ch. Meyer
- Formal Verification of a Commercial Smart Card Applet with Multiple Toolsby: Bart Jacobs, Claude Marché, Nicole Rauch
- Verifying Invariants of Component-Based Systems through Refinementby: Olga Kouchnarenko, Arnaud Lanoix
- Glass Box and Black Box Views of State-Based System Specifications.by: Michel Bidoit, Rolf Hennicker
- Modular Rewriting Semantics of Programming Languagesby: José Meseguer, Christiano Braga
- A Science of Software Designby: Don S. Batory
- Abstraction for Safety, Induction for Livenessby: Muffy Calder
- Expressing Iterative Properties Logically in a Symbolic Settingby: Carron Shankland, Jeremy Bryans, Lionel Morel
- Deductive Verification of Distributed Groupware Systemsby: Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch
- Proof Support for RAISE by a Reuse Approach Based on Institutionsby: Morten P. Lindegaard, Anne Elisabeth Haxthausen
- Linear Temporal Logic and Z Refinementby: John Derrick, Graeme Smith
- A Hybrid Logic of Knowledge Supporting Topological Reasoningby: Bernhard Heinemann
- A Language for Configuring Multi-level Specificationsby: Gillian Hill, Steven Vickers
- Towards Correspondence Carrying Specificationsby: Marius C. Bujorianu, Eerke A. Boiten
- Formalizing and Proving Semantic Relations between Specifications by Reflectionby: Manuel Clavel, Narciso Martí-Oliet, Miguel Palomino
- A Generic Software Safety Document Generatorby: Ewen Denney, Ram Prasad Venkatesan
- Counting Votes with Formal Methodsby: Bart Jacobs
- A Formally Verified Calculus for Full Java Cardby: Kurt Stenzel
- Extending Separation Logic with Fixpoints and Postponed Substitutionby: Élodie-Jane Sims
- State Space Reduction for Process Algebra Specificationsby: Hubert Garavel, Wendelin Serwe
- Techniques for Executing and Reasoning about Specification Diagramsby: Prasanna Thati, Carolyn L. Talcott, Gul Agha
- Abstract Domains for Property Checking Driven Analysis of Temporal Propertiesby: Damien Massé
- Modal Abstractions in µCRLby: Jaco van de Pol, Miguel Valero Espada
- Refining Mobile UML State Machinesby: Alexander Knapp, Stephan Merz, Martin Wirsing
- Separate Compositional Analysis of Class-Based Object-Oriented Languagesby: Francesco Logozzo
- Modularity and the Rule of Adaptationby: Cees Pierik, Frank S. de Boer
- Verifying a Sliding Window Protocol in µCRLby: Wan Fokkink, Jan Friso Groote, Jun Pang, Bahareh Badban, Jaco van de Pol
- Model-Checking Systems with Unbounded Variables without Abstractionby: Magali Contensin, Laurence Pierre
- On Refinement of Generic State-Based Software Componentsby: Sun Meng, Luís Soares Barbosa
- Formalising Graphical Behaviour Descriptionsby: Kenneth J. Turner
- Semantics of Plan Revision in Intelligent Agentsby: Birna van Riemsdijk, John-Jules Ch. Meyer, Frank S. de Boer
- Flexible Proof Reuse for Software Verificationby: Chris Hunter, Peter Robinson, Paul A. Strooper
- Modal Kleene Algebra and Partial Correctnessby: Bernhard Möller, Georg Struth
- Generic Exception Handling and the Java Monadby: Lutz Schröder, Till Mossakowski
- Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptionsby: Farn Wang
- Behavioural Types and Component Adaptationby: Antonio Brogi, Carlos Canal, Ernesto Pimentel
- Abstracting Call-Stacks for Interprocedural Verification of Imperative Programsby: Bertrand Jeannet, Wendelin Serwe
- On Guard: Producing Run-Time Checks from Integrity Constraintsby: Michael Benedikt, Glenn Bruns
- A Foundation of Escape Analysisby: Patricia M. Hill, Fausto Spoto
- Modelling Concurrent Behaviours by Commutativity and Weak Causality Relationsby: Guangyuan Guo, Ryszard Janicki
- Removing Redundant Arguments of Functionsby: María Alpuente, Santiago Escobar, Salvador Lucas
- Algebraic Dynamic Programmingby: Robert Giegerich, Carsten Meyer
- Pragmatics of Modular SOSby: Peter D. Mosses
- Class-Based versus Object-Based: A Denotational Comparisonby: Bernhard Reus
- On Bisimulations for the Spi Calculusby: Johannes Borgström, Uwe Nestmann
- Higher-Order Quantification and Proof Searchby: Dale Miller
- Fully Automatic Adaptation of Software Components Based on Semantic Specificationsby: Christian Haack, Brian Howard, Allen Stoughton, J. B. Wells
- On Solving Temporal Logic Queriesby: Samuel Hornus, Ph. Schnoebelen
- Vacuity Checking in the Modal Mu-Calculusby: Yifei Dong, Beata Sarna-Starosta, C. R. Ramakrishnan, Scott A. Smolka
- Automata and Games for Synthesisby: Igor Walukiewicz
- Equational Axioms for Probabilistic Bisimilarityby: Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir
- A Class of Decidable Parametric Hybrid Systemsby: Michaël Adélaïde, Olivier Roux
- Bisimulation by Unificationby: Paolo Baldan, Andrea Bracciali, Roberto Bruni
- Algebraic Support for Service-Oriented Architectureby: José Luiz Fiadeiro
- Revisiting the Categorical Approach to Systemsby: Antónia Lopes, José Luiz Fiadeiro
- Guarded Transitions in Evolving Specificationsby: Dusko Pavlovic, Douglas R. Smith
- From Specifications to Code in CASLby: David Aspinall, Donald Sannella
- HASCASL: Towards Integrated Specification and Development of Functional Programsby: Lutz Schröder, Till Mossakowski
- An Algebra of Non-safe Petri Boxesby: Raymond R. Devillers, Hanna Klaudel, Maciej Koutny, Franck Pommereau
- Tool-Assisted Specification and Verification of the JavaCard Platformby: Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa
- A Theory of May Testing for Asynchronous Calculi with Locality and No Name Matchingby: Prasannaa Thati, Reza Ziaei, Gul Agha
- Extending JML Specifications with Temporal Logicby: Kerry Trentelman, Marieke Huisman
- Proof Transformations for Evolutionary Formal Software Developmentby: Axel Schairer, Dieter Hutter
- A Framework for Order-Sorted Algebraby: John G. Stell
- Refusal Simulation and Interactive Gamesby: Irek Ulidowski
- Specifying and Verifying a Decimal Representation in Java for Smart Cardsby: Cees-Bart Breunesse, Bart Jacobs, Joachim van den Berg
- The Development Graph Manager MAYAby: Serge Autexier, Dieter Hutter, Till Mossakowski, Axel Schairer
- BRAIN : Backward Reachability Analysis with Integersby: Tatiana Rybina, Andrei Voronkov
- Sharing Objects by Read-Only Referencesby: Mats Skoglund
- A Method for Secure Smartcard Applicationsby: Dominik Haneberg, Wolfgang Reif, Kurt Stenzel
- Analyzing String Buffers in Cby: Axel Simon, Andy King
- Transforming Processes to Check and Ensure Information Flow Securityby: Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi
- Analysis of Downward Closed Properties of Logic Programsby: Patricia M. Hill, Fausto Spoto
- A Modal Logic for KLAIMby: Rocco De Nicola, Michele Loreti
- Invited Talk: A Software Engineering Program of Lasting Valueby: David Lorge Parnas
- Maude Action Tool: Using Reflection to Map Action Semantics to Rewriting Logicby: Christiano de O. Braga, Edward Hermann Haeusler, José Meseguer, Peter D. Mosses
- Meta Languages in Algebraic Compilersby: Eric Van Wyk
- Invited Talk: Plugging Data Constructs into Paradigm-Specific Languages: Towards an Application to UMLby: Egidio Astesiano, Maura Cerioli, Gianna Reggio
- Kleene under a Demonic Starby: Jules Desharnais, Bernhard Möller, Fairouz Tchier
- A Reuse-Oriented Framework for Hierarchical Specificationsby: Sophie Coudert, Pascale Le Gall
- Behavioural Subtyping Relations for Object-Oriented Formalismsby: Clemens Fischer, Heike Wehrheim
- Invited Talk: Algebraic State Machinesby: Manfred Broy, Martin Wirsing
- Invited Talk: Weaving Formal Methods into the Undergraduate Computer Science Curriculumby: Jeannette M. Wing
- Invited Talk: ASM Formalware in the Software Engineering Cycleby: Yuri Gurevich
- Distance Functions for Defaults in Reactive Systemsby: Sofia Guerra
- Step by Step to Historiesby: Max Breitling, Jan Philipps
- CASL-CHART: A Combination of Statecharts and of the Algebraic Specification Language CASLby: Gianna Reggio, Lorenzo Repetto
- A Global Semantics for Viewsby: Christine Choppy, Pascal Poizat, Jean-Claude Royer
- Approximate Bisimilarityby: Mingsheng Ying, Martin Wirsing
- Process Calculi for Coordination: From Linda to JavaSpacesby: Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro
- Invited Talk: Applying Category Theory to Derive Engineering Software from Encoded Knowledgeby: Michael Healy, Keith E. Williamson
- Message Authentication through Non Interferenceby: Riccardo Focardi, Roberto Gorrieri, Fabio Martinelli
- Testing from Structured Algebraic Specificationsby: Patrícia D. L. Machado
- The Extensibility of Maude's Module Algebraby: Francisco Durán
- Extended Institutions for Testingby: Marielle Doche, Virginie Wiels
- An ASM Semantics for UML Activity Diagramsby: Egon Börger, Alessandra Cavarra, Elvinia Riccobene
- Making Mathematical Methods More Practical for Software Developers (Invited Talk)by: David Lorge Parnas
- MIX(FL): A Kernel Language of Mixin Modulesby: Davide Ancona
- Time and Probability in Process Algebraby: Suzana Andova
- Practical Application of Functional and Relational Methods for the Specification and Verification of Safety Critical Softwareby: Mark Lawford, Jeff McDougall, Peter Froebel, Greg Moum
- Random Access to Abstract Data Typesby: Martin Erwig
- The Algebra of Multi-taskingby: Colin J. Fidge
- A Causal Semantics for Timed Default Concurrent Constraint Programmingby: Simone Tini, Andrea Maggiolo-Schettini
- Process Algebra versus Axiomatic Specification of a Real-Time Protocolby: Antonio Cerone
- Invited Talk: Pointwise Relational Programmingby: Oege de Moor, Jeremy Gibbons
- Towards a Toolkit for Actor System Specificationby: Carolyn L. Talcott
- A New Logic for Electronic Commerce Protocolsby: Kamel Adi, Mourad Debbabi, Mohamed Mejri
- Generalizing the Modal and Temporal Logic of Linear Timeby: Bernhard Heinemann
- A Monad for Basic Java Semanticsby: Bart Jacobs, Erik Poll
- Abstract Interpretation of Prolog Programsby: Fausto Spoto, Giorgio Levi
- Systematising Reactive System Designby: T. S. E. Maibaum, Pauline Kan, Kevin Lano
- Condensing Lemmas for Pure Type Systems with Universesby: Blas C. Ruiz Jiménez
- Abstraction Barriers in Equational Proofby: Jo Erskine Hannay
- A Synergy Between Model-Checking and Type Inference for the Verification of Value-Passing Higher-Order Processesby: Mourad Debbabi, Abdelkader Benzakour, Béchir Ktari
- RECOPLA: An Extendible Graphic Meta-Editorby: Zoltan Gassmann, Luis Mandel, Roshan Sembacuttiaratchy
- Interpolation in Modal Logicby: Maarten Marx
- Effective Recognizability and Model Checking of Reactive Fiffo Automataby: Grégoire Sutre, Alain Finkel, Olivier Roux, Franck Cassez
- The ABACO System - An Algebraic Based Action COmpilerby: Hermano Perrelli de Moura, Luis Carlos de Sousa Menezes
- Algebraic Specifications, Higher-Order Types, and Set-Theoretic Modelsby: Hélène Kirchner, Peter D. Mosses
- Verification of Temporal Properties of Processes in a Setting with Databy: Jan Friso Groote, Radu Mateescu
- Systematic Design of Call-Coverage Featuresby: Pamela Zave
- A Single Perspective on Arrows between Institutionsby: Alfio Martini, Uwe Wolter
- The State of PEPby: Bernd Grahlmann
- Combining Methods for the Livelock Analysis of a Fault-Tolerant Systemby: Bettina Buth, Jan Peleska, Hui Shi
- On Oracles for Interpreting Test Results against Algebraic Specificationsby: Patrícia D. L. Machado
- A Logic for Real-Time Systems Specification, Its Algebraic Semantics, and Equational Calculusby: Gabriel Baum, Marcelo F. Frias, T. S. E. Maibaum
- Verification of Bounded Delay Asynchronous Circuits with Timed Tracesby: Tomohiro Yoneda, Bin Zhou, Bernd-Holger Schlingloff
- An Algebraic View of Program Compositionby: Pietro Cenciarelli
- Improving Computations in a Typed Functional Logic Languageby: Jesús Manuel Almendros-Jiménez
- Pi-Congruences as CCS Equivalencesby: Paola Quaglia
- Scheduling Algebraby: Rob J. van Glabbeek, Peter Rittgen
- Categorical Programming with Abstract Data Typesby: Martin Erwig
- Duration Calculus, a Logical Approach to Real-Time Systemsby: Zhou Chaochen
- Observational Logicby: Rolf Hennicker, Michel Bidoit
- Consistency of Partial Process Specificationsby: Maarten Steen, John Derrick, Eerke A. Boiten, Howard Bowman
- Term Rewriting in a Logic of Special Relationsby: W. Marco Schorlemmer
- Visual Abstractions for Temporal Verificationby: Zohar Manna, Anca Browne, Henny Sipma, Tomás E. Uribe
- Abstract Algebraic Logicby: Don Pigozzi
- A Trace-Based Refinement Calculus for Shared-Variable Parallel Programsby: Jürgen Dingel
- A Linear Metalanguage for Concurrencyby: Glynn Winskel
- Algebraic Semantics of Coordination or What Is in a Signatureby: José Luiz Fiadeiro, Antónia Lopes
- Building Models of Linear Logicby: Valeria de Paiva, Andrea Schalk
- Separating Sets by Modal Formulasby: Bernhard Heinemann
- An Algebraic Approach to Combining Processes in a Hardware/Software Partitioning Environmentby: Leila Silva, Augusto Sampaio, Edna Barros, Juliano Iyoda
- Type Analysis for CHIPby: Wlodzimierz Drabent, Pawel Pietrzak
- Factorizing Equivalent Variable Pairs in ROBDD-Based Implementations of Posby: Roberto Bagnara, Peter Schachte
- Architectural Specifications in CASLby: Michel Bidoit, Donald Sannella, Andrzej Tarlecki
- Modular Refinement and Model Buildingby: Martin de Groot, Ken Robinson
- PAMELA + PVSby: Bettina Buth
- Abstract Interpretation of Algebraic Polynomial Systems (Extended Abstract)by: Patrick Cousot, Radhia Cousot
- Case Studies in Using a Meta-Method for Formal Method Integrationby: Richard F. Paige
- A Linear Temporal Logic Approach to Objects with Transactionsby: Grit Denker, Jaime Ramos, Carlos Caleiro, Amílcar Sernadas
- Analysing Multi-Agent System Traces with IDaFby: C. K. Low
- Parametric Analysis of Computer Systemsby: Farn Wang, Pao-Ann Hsiung
- Model Checking and Fault Toleranceby: Glenn Bruns, Ian Sutherland
- An Algebraic Language Processing Environmentby: Teodor Rus, Tom Halverson, Eric Van Wyk, Robert Kooima
- ATM Switch Design: Parametric High-Level Modeling and Formal Verificationby: Sreeranga P. Rajan, Masahiro Fujita
- Recording HOL Proofs in a Structured Browsable Formatby: Jim Grundy, Thomas Långbacka
- Invariants of Parameterized Binary Tree Networks as Greatest Fixpointsby: David Lesens
- Verification of Distributed Real-Time and Fault-Tolerant Protocolsby: Jozef Hooman
- Software Design, Specification, and Verification: Lessons Learned from the Rether Case Studyby: Xiaoqun Du, Kevin T. McDonnell, Evangelos Nanos, Y. S. Ramakrishna, Scott A. Smolka
- Invariants, Bisimulations and the Correctness of Coalgebraic Refinementsby: Bart Jacobs
- Head-Tactics Simplificationby: Yves Bertot
- Iteration 2-Theories: Extended Abstractby: Stephen L. Bloom, Anna Labella, Zoltán Ésik, Ernest G. Manes
- On the Specification and Verification of Performance Properties for a Timed Process Algebraby: Xiao Jun Chen, Flavio Corradini
- Permissive Subsorted Partial Logic in CASLby: Maura Cerioli, Anne Elisabeth Haxthausen, Bernd Krieg-Brückner, Till Mossakowski
- Completeness in Abstract Interpretation: A Domain Perspectiveby: Roberto Giacobazzi, Francesco Ranzato
- Algebraic Composition and Refinement of Proofsby: Martin Simons, Michel Sintzoff
- The B Method and the B Toolkitby: Ken Robinson
- Selective Attribute Elimination for Categorial Data Specificationsby: Frank Piessens, Eric Steegmans
- The Circal Systemby: Antonio Cerone, Alex J. Cowie, George J. Milne
- Software Configuration with Information Systemsby: Slim Ben Lamine, John Plaice
- DOVE: A Tool for Design Oriented Verification and Evaluationby: Maris A. Ozols, Katherine A. Eastaughffe, Anthony Cant
- Representing Place/Transition Nets in Span(Graph)by: Piergiulio Katis, Nicoletta Sabadini, Robert F. C. Walters
- Modelling Specification Construction by Successive Approximationsby: Nicole Lévy, Jeanine Souquières
- Extending Process Languages with Timeby: Irek Ulidowski, Shoji Yuen
- Preservation and Reflection in Specificationby: Antónia Lopes, José Luiz Fiadeiro
- Specification of Timing Constraints within the Circal Process Algebraby: Antonio Cerone, George J. Milne
- On Bisimulation, Fault-Monotonicity and Provable Fault-Toleranceby: Tomasz Janowski
- From Sequential to Multi-Threaded Java: An Event-Based Operational Semanticsby: Pietro Cenciarelli, Alexander Knapp, Bernhard Reus, Martin Wirsing
- On Partial Validation of Logic Programsby: Sébastien Limet, Frédéric Saubion
- The Hidden Function Question Revisitedby: Arno Schönegge
- Refinement Rules for Real-Time Multi-tasking Programsby: Colin J. Fidge
- The Cogito Development Systemby: Owen Traynor, Dan Hazel, Peter Kearney, Andrew Martin, Ray Nickson, Luke Wildman
- The Update Calculus (Extended Abstract)by: Joachim Parrow, Björn Victor
- CAMILA: Prototyping and Refinement of Constructive Specificationsby: J. J. Almeida, Luís Soares Barbosa, F. L. Neves, José Nuno Oliveira
- Rigorous Object-Oriented Modeling: Integrating Formal and Informal Notationsby: Robert B. France, Jean-Michel Bruel, Maria M. Larrondo-Petrie, E. Grant
- Synchronization of Logics with Mixed Rules: Completeness Preservationby: Amílcar Sernadas, Cristina Sernadas, Carlos Caleiro
- Deadlock Analysis for a Fault-Tolerant Systemby: Bettina Buth, Michel Kouvaras, Jan Peleska, Hui Shi
- Ensuring Streams Flowby: Alastair Telford, David Turner
- Refinement-Type Checker for Standard MLby: Rowan Davies
- Floating Point Verification in HOL Light: The Exponential Functionby: John Harrison
- Symbolic Bisimulation for Full LOTOSby: Carron Shankland, Muffy Thomas
- Span(Graph): A Categorial Algebra of Transition Systemsby: Piergiulio Katis, Nicoletta Sabadini, Robert F. C. Walters
- Pushouts of Order-Sorted Algebraic Specificationsby: Anne Elisabeth Haxthausen, Friederike Nickl
- Algebraic Specification of Reactive Systemsby: Manfred Broy
- A Model for Mobile Point-to-Point Data-flow Networks without Channel Sharingby: Radu Grosu, Ketil Stølen
- ASD: The Action Semantic Description Toolsby: Arie van Deursen, Peter D. Mosses
- A Study on the Specification and Verification of Performance Properties (Extended Abstract)by: Xiao Jun Chen, Flavio Corradini, Roberto Gorrieri
- Towards Integrating Algebraic Specification and Functional Programming: the Opal System (Extended Abstract)by: Klaus Didrich, Carola Gerke, Wolfgang Grieskamp, Christian Maeder, Peter Pepper
- Algebraic View Specificationby: Barbara Paech
- CtCoq: A System Presentationby: Janet Bertot, Yves Bertot
- A Logic-Based Technology to Mechanize Software Components Reuseby: Patrick Parot
- Semantic Foundations for Embedding HOL in Nuprlby: Douglas J. Howe
- Constructive Semantics of Esterel: From Theory to Practice (Abstract)by: Gérard Berry
- Some Characteristics of Strong Innermost Normalizationby: M. R. K. Krishna Rao
- The FC2TOOLS Setby: Amar Bouali, Annie Ressouche, Valérie Roy, Robert de Simone
- Towards Heterogeneous Formal Specificationby: Gilles Bernot, Sophie Coudert, Pascale Le Gall
- An Equational Axiomatization of Observation Congruence for Prefix Iterationby: Luca Aceto, Anna Ingólfsdóttir
- Incremental Formalizationby: Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun
- Coalgebraic Specifications and Models of Determinatistic Hybrid Systemsby: Bart Jacobs
- On the Completeness of the Euations for the Kleene Star in Bisimulationby: Wan Fokkink
- Resolution of Goals with the Functional and Logic Programming Language LPG: Impact of Abstract Interpretationby: Didier Bert, Rachid Echahed, Kamel Adi
- Two Industrial Trials of Formal Specificationby: John S. Fitzgerald
- PROPLANE: A Specification Development Environmentby: Jeanine Souquières, Nicole Lévy
- Formal Verification of SIGNAL Programs: Application to a Power Transformer Station Controllerby: Michel Le Borgne, Hervé Marchand, Éric Rutten, Mazen Samaan
- Using Heterogeneous Formal Methods in Distributed Software Engineering Educationby: Bernd J. Krämer
- InterACT: An Interactive Theorem Prover for Algebraic Specificationsby: Robert Geisler, Marcus Klar, Felix Cornelius
- Combining Reductions and Computations in ReDuXby: Reinhard Bündgen, Werner Lauterbach
- TkGofer: A Functional GUI Libraryby: Wolfram Schulte, Thilo Schwinn, Ton Vullinghs
- ECHIDNA: A System for Manipulating Explicit Choice Higher Dimensional Automataby: Richard Buckland, Michael Johnson
- A Bounded Retransmission Protocol for Large Data Packetsby: Jan Friso Groote, Jaco van de Pol
- Applying Research Results in the Industrial Environment: the Case of the TRIO Specification Languageby: Dino Mandrioli
- Programming in Lygon: An Overviewby: James Harland, David J. Pym, Michael Winikoff
- The TOOLBUS Coordination Architecture - A Demonstrationby: Paul Klint, Pieter A. Olivier
- Using Occurence and Evolving Algebras for the Specification of Language-Based Programming Toolsby: Arnd Poetzsch-Heffter
- A Categorical Characterization of Consistency Resultsby: Christel Baier, Mila E. Majster-Cederbaum
- Programming in Lygon: A System Demonstrationby: James Harland, David J. Pym, Michael Winikoff
- On the Emergence of Properties in Component-Based Systemsby: José Luiz Fiadeiro
- ALPHA - A Class Library for a Metamodel Based on Algebraic Graph Theoryby: Sebastian Erdmann, Ingo Claßen
- Free Variable Tableaux for a Many Sorted Logic with Preordersby: Antonio Gavilanes, Javier Leach, Susana Nieva
- A New Proof-Manager and Graphic Interface for the Larch Proverby: Frédéric Voisin
- Industrial Applications of ASF+SDFby: Mark van den Brand, Arie van Deursen, Paul Klint, Steven Klusener, Emma van der Meulen
- The TYPELAB Specification and Verification Environmentby: Friedrich W. von Henke, Marko Luther, Holger Pfeifer, Harald Rueß, Detlef Schwier, Martin Strecker, Matthias Wagner
- Boolean Formalism and Explanationsby: Eric C. R. Hehner
- A Formal Framework for Modules with Stateby: Davide Ancona, Elena Zucca
- Conditional Directed Narrowingby: Sébastien Limet, Pierre Réty
- Toward a Classification Approach to Designby: Douglas R. Smith
- Proving Existential Termination of Normal Logic Programsby: Massimo Marchiori
- The Discrete Time TOOLBUSby: Jan A. Bergstra, Paul Klint
- Using Ghost Variables to Prove Refinementby: Monica Marcus, Amir Pnueli
- Finite Axiom Systems for Testing Preorder and De Simone Process Languagesby: Irek Ulidowski
- Verification Using PEPby: Stephan Melzer, Stefan Römer, Javier Esparza
- Introducing Formal Methods to Software Engineers Through OMG's COBRA Environment and Interface Definition Languageby: Sriram Sankar
- Object-Oriented Implementation of Abstract Data Type Specificationsby: Rolf Hennicker, Christoph Schmitz II
- Approximative Analysis by Process Algebra with Graded Spatial Actionsby: Yoshinao Isobe, Yutaka Sato, Kazuhito Ohmaki
- Preprocessing for Invariant Validationby: E. Pascal Gribomont
- Tracing the Origins of Verification Conditionsby: Ranan Fraer
- Symbolic Bisimulation for Timed Processesby: Michele Boreale
- TERSE: A Visual Environment for Supporting Analysis, Verification and Transformation of Term Rewriting Systemsby: Nobuo Kawaguchi, Toshiki Sakabe, Yasuyoshi Inagaki
- The Embedded Software of an Electrical Meter: An Experiment in Using Formal Methods in an Industrial Projectby: André Arnold, Didier Bégay, Jean-Pierre Radoux
- Automating Induction over Mutually Recursive Functionsby: Deepak Kapur, M. Subramaniam
- SPECWARE: An Advanced Evironment for the Formal Development of Complex Software Systemsby: Richard Jüllig, Yellamraju V. Srinivas, J. Liu
- ASSPEQUIE: An Integrated Specification Environment Providing Inter-Operability of Toolsby: Michel Bidoit, Christine Choppy, Frédéric Voisin
- Verification of Logic Programs with Delay Declarationsby: Krzysztof R. Apt, Ingrid Luitjes
- Representing, Verifying and Applying Software Development Steps using the PVS Systemby: Axel Dold
- On Mechanizing Proofs within a Complete Proof System for Unityby: Naima Brown, Abdelillah Mokkedem
- Knowledge Based Computation (Extended Abstract)by: Rohit Parikh
- Encoding Natural Semantics in Coqby: Delphine Terrasse
- SEAMLESS: Knowledge Based Evolutionary System Synthesisby: Jutta Eusterbrock
- On the Decidability of Process Equivalences for the pi-calculusby: Mads Dam
- Causality and True Concurrency: A Data-flow Analysis of the Pi-Calculus (Extended Abstract)by: Lalita Jategaonkar Jagadeesan, Radha Jagadeesan
- Detecting Isomorphisms of Modular Specifications with Diagramsby: Catherine Oriat
- Mongruences and Cofree Coalgebrasby: Bart Jacobs
- Order-sorted Algebraic Specifications with Higher-order Functionsby: Anne Elisabeth Haxthausen
- The Role of Education and Trainig in the Industrial Application of Formal Methodsby: Ted Ralston, Susan L. Gerhart, Dan Craigen
- A Declarative System for Multi-database Interoperabilityby: Laks V. S. Lakshmanan, Iyer N. Subramanian, Despina Papoulis, Nematollaah Shiri
- Petri Nets, Traces, and Local Model Checkingby: Allan Cheng
- Teaching Mathematics to Software Engineersby: Jeannette M. Wing
- An Introduction to Category-based Equational Logicby: Joseph A. Goguen, Razvan Diaconescu
- An Object-Oriented Front-end for Deductive Databasesby: Hasan M. Jamil, Laks V. S. Lakshmanan
- Proving the Correctness of Behavioural Implementationsby: Michel Bidoit, Rolf Hennicker
- Logical Foundations for Compositional Verification and Development of Concurrent Programs in UNITYby: Pierre Collette, Edgar Knapp
- CPO Models for Infinite Term Rewritingby: Andrea Corradini, Fabio Gadducci
- Information Algebrasby: Ewa Orlowska
- Higher-Order Narrowing with Convergent Systemsby: Christian Prehofer
- An Algebraic Construction of the Well-Founded Modelby: Rajiv Bagai, Rajshekhar Sunderraman
- An Algebraic Development Technique for Information Systemsby: Martin Gogolla, Rudolf Herzig
- Confluence in Concurrent Constraint Programmingby: Moreno Falaschi, Maurizio Gabbrielli, Kim Marriott, Catuscia Palamidessi
- The METAGEN Systemby: Houari A. Sahraoui
- Dynamic Matrices and the Cost Analysis of Concurrent Programsby: Gian Luigi Ferrari, Ugo Montanari
- Context-Free Event Domains are Recognizableby: Eric Badouel, Philippe Darondeau, Jean-Claude Raoult
- An Algebraic Framework for Developing and Maintaining Real-Time Systemsby: Elizabeth I. Leonard, Amy E. Zwarico
- Specification of the Unix File System: A Comparative Case Studyby: Maritta Heisel
- Semantic Typing for Parametric Algebraic Specificationsby: María Victoria Cengarle
- Verification in Continuous Time by Discrete Reasoningby: Luca de Alfaro, Zohar Manna
- The SuRE Programming Frameworkby: Bharat Jayaraman, Kyonghee Moon
- A Generic Algebra for Data Collections Based on Constructive Logicby: P. Rajagopalan, C. P. Tsang
- A Calculus of Countable Broadcasting Systemsby: Yoshinao Isobe, Yutaka Sato, Kazuhito Ohmaki
- Partial Order Programming (Revisited)by: Bharat Jayaraman, Mauricio Osorio, Kyonghee Moon
- SPIKE: A System for Automatic Inductive Proofsby: Adel Bouhoula, Michaël Rusinowitch
- Completeness Results for Two-sorted Metric Temporal Logicsby: Angelo Montanari, Maarten de Rijke
- Automated Reasoning About Parallel Algorithms Using Powerlistsby: Deepak Kapur, Mahadevan Subramaniam
- A Framework for Machine-Assisted User Interface Verificationby: Peter Bumbulis, Paulo S. C. Alencar, Donald D. Cowan, Carlos José Pereira de Lucena
- Symbolic Timing Devicesby: Anne Bergeron
- Equational Logic as a Toolby: David Gries
- Executing Action Semantic Descriptions using ASF+SDFby: Arie van Deursen, Peter D. Mosses
- Towards an Integrated Environment for Concurrent programs Developmentby: Naima Brown, Dominique Méry
- On the Coverage of Partial Validationsby: Ed Brinksma
- On the Correctness of Modular Systemsby: Marisa Navarro, Fernando Orejas, Ana Sánchez
- Category Theory for the Configuration of Complex Systemsby: Gillian Hill
- The Role of Memory in Object-based and Object-oriented Languagesby: Eric G. Wagner
- A Notion of Refinement for Automataby: Nicoletta Sabadini, Sebastiano Vigna, Robert F. C. Walters
- Towards an Algebraic Theory of Inheritance in Project Oriented Programmingby: Xue-Miao Lu, Tharam S. Dillon
- Parameterized Recursion Theory - A Tool for the Systematic Classification of Specification Methodsby: Till Mossakowski
- Translation Results for Modal Logics of Reactive Systemsby: François Laroussinie, Sophie Pinchinat, Ph. Schnoebelen
- Full Abstraction in Structural Operational Semantics (Extended Abstract)by: Rob J. van Glabbeek
- Verifying Communication Protocols Via Testing-Projectionby: Khalil Drira, Pierre Azéma
- Equivalences of Transition Systems in an Algebraic Frameworkby: Pasquale Malacaria
- RALF - A Relation-Algebraic Formula Manipulation System and Proof Checkerby: Claudia Hattensperger, Rudolf Berghammer, Gunther Schmidt
- The LOTOS Toolboxby: Thony van der Vloedt
- Abstract and Concrete Objects - An Algebraic Design Method for Object-Based Systemsby: Ruth Breu, Michael Breu
- Comparing Two Different Approaches to Products in Abstract Relation Algebraby: Rudolf Berghammer, Armando Martin Haeberer, Gunther Schmidt, Paulo A. S. Veloso
- The ASF+SDF Meta-environmentby: Arie van Deursen, T. B. Dinesh, Emma van der Meulen
- On Using a Composition Principle to Design Parallel Programsby: Abdelillah Mokkedem, Dominique Méry
- Constraints in Term Algebras (Short Survey)by: Hubert Comon
- Interaction between Algebraic Specification Grammars and Modular System Designby: Hartmut Ehrig, Francesco Parisi-Presicce
- A Coherent Type System for a Concurrent, Functional and Imperative Programming Languageby: Dominique Bolignano, Mourad Debbabi
- An Object-Oriented Design for the ACT ONE Environmentby: Martin Gogolla, Ingo Claßen
- An Overview of the SODA Systemby: Peter Thiemann
- Automated Proof of the Correctness of a Compiling Specificationby: Elizabeth A. Scott
- Real-Time Program Synthesis from Specificationsby: Aurel Cornell, John Knaack, A. Nangia, Teodor Rus
- Dimension-Complemented Lambda Abstraction Algebrasby: Don Pigozzi, Antonino Salibra
- Synchronous Observers and the Verification of Reactive Systemsby: Nicolas Halbwachs, Fabienne Lagnier, Pascal Raymond
- Joining Abstract and Concrete Computations in Constraint Logic Programmingby: Roberto Giacobazzi, Giorgio Levi, Saumya K. Debray
- Algebraic-Oriented Institutionsby: Maura Cerioli, Gianna Reggio
- Applying Algebraic Logic to Logicby: Hajnal Andréka, István Németi, Ildikó Sain
- Specification of Hybrid Systems in CRPby: R. K. Shyamasundar
- An Algebraic Approach to Modeling in Software Engineeringby: George Loegel, Chinya V. Ravishankar
- Modal Action Logic in a Practical Specification Languageby: Ismar Neumann Kaufman, Silvio Romero de Lemos Meira
- Increasing the Level of Abstraction in Traditional Functional Languages by Using Compile-time Reflectionby: Tim Sheard
- Specifying Type Systems with Multi-Level Order-Sorted Algebraby: Martin Erwig
- Completeness of Equational Definitions over Predefined Algebrasby: Valentin M. Antimirov, Anatoli Degtyarev
- On the Value of Commutative Diagrams in Information Modellingby: Michael Johnson, Christopher N. G. Dampney
- A Characterization of LOTOS Representable Networks of Parallel Processesby: David de Frutos-Escrig
- Rigorous Specification of Real-Time Systemsby: Steve Schneider
- Semantics Frameworks for a Class of Modular Algebraic Netsby: Eugenio Battiston, V. Crespi, Fiorella de Cindio, Giancarlo Mauri
- A Formal Definition of an Abstract Prolog Compiler (Extended Abstract)by: Julio García-Martín, Juan José Moreno-Navarro
- Towards Performance Evaluation in Process Algebrasby: Roberto Gorrieri, Marco Roccetti
- Peirce Algebrasby: Chris Brink, Katarina Britz
- Relation Algebras for Reasoning about Time and Spaceby: Roger D. Maddux
- RELVIEW - A Computer System for the Manipulation of Relationsby: Rudolf Berghammer, Gunther Schmidt
- On Adding Algebraic Theories with Induction to Typed Lambda Calculiby: Val Breazu-Tannen, Ramesh Subrahmanyam
- Proving the Correctness of Algebraically Specified Software: Modularity and Observability Issuesby: Gilles Bernot, Michel Bidoit
- Language Polynomial in the Input Plus Outputby: Jiazhen Cai, Robert Paige
- Using Algebraic Specification in Floyd-Hoare Assertionsby: Hantao Zhang, Angshuman Guha, Xin Hua
- A Case Study Towards Algebraic Verification of Codeby: Heinrich Hussmann
- ACT TWO: An Algebraic Module Specification and Interconnection Languageby: Werner Fey
- Integration of Semantical Verification Conditions in a Specification Language Definitionby: Didier Bert, Christine Lafontaine
- A Framework for Dexterous Manipulation using Lie Algebrasby: Daniela Rus
- A Formal Approach to Software Testingby: Gilles Bernot, Marie-Claude Gaudel, Bruno Marre
- The PROSPECTRA System: A Unified Development Frameworkby: Einar W. Karlsen, Bernd Krieg-Brückner, Owen Traynor
- Selecting Reusable Components Using Algebraic Specificationsby: David Eichmann
- Decomposition of Finite State Machines under Isomorphic and Bisimulation Equivalencesby: Huajun Qin, Philip Lewis
- Event Spaces and their Linear Logicby: Vaughan R. Pratt
- Algebraic Semantics of Real-Time Process Specificationsby: Gil Zvi Deutsch, S. Kaplan
- Polynomial Relators (Extended Abstract)by: Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, Jaap van der Woude
- The Combination of Specifications and the Induced Relations in Object Oriented Programsby: G. Steve Hirst, T. B. Dinesh
- Pattern Matching: A Sheaf-Theoretic Approachby: Yellamraju V. Srinivas
- Solving Divergence in Knuth-Bendix Completion by Enriching Signaturesby: Muffy Thomas, Phil Watson
- Efficient Algebraic Operations on Programsby: Neil D. Jones
- MEC: A System for Constructing and Analysis Transition Systemsby: André Arnold
- Structure of Concurrencyby: Ryszard Janicki, Maciej Koutny
- Modification Algebrasby: G. Ramalingam, Thomas W. Reps
- An Algebraic Semantics for the Specification Language Z++by: Kevin Lano, Howard P. Haughton
- On the Reusability of Specifications and Implementationsby: Francesco Parisi-Presicce
- Type Consistency Checking for Concurrent Independent Processesby: Aurel Cornell
- Modeling Concurrency with AND/OR Algebraic Theoriesby: Maria Zamfir Bleyberg
- Theory of Algebraic Module Specification including Behavioral Semantics and Constraintsby: Hartmut Ehrig, Michael Baldamus, Felix Cornelius, Fernando Orejas
- Extracting Recursive Programs in Type Theoryby: Scott F. Smith
- Algebraic Construction of Program Representation Graphsby: Richard Marciano, Teodor Rus
- Algebraic Specification at Workby: Egidio Astesiano, Alessandro Giovini, Franco Morando, Gianna Reggio
- On Rewriting Behavioral Semantics in Process Algebrasby: Paola Inverardi, Monica Nesi
- Deriving Incremental Implementations from Algebraicby: Emma van der Meulen
- Tools for Algebraic Distributed System Designby: Henk Eertink
- TwoLev: A Two Level Scannerby: John Knaack, Teodor Rus
- Clean Algebraic Exception with Implicit Propagationby: Pierre-Yves Schobbens
- Towards a Theory of Binding Structures: An Abstract Algebraby: Carolyn L. Talcott
- About Algebras, Fixpoints and Semanticsby: Irène Guessarian
- Studies on the Ground Convergence Property of Conditional Theoriesby: Emmanuel Kounalis, Michaël Rusinowitch
![[SWISH++]](/docis/swish-powered.gif){kind=small}
