Bernhard K. Aichernig, Bernhard Beckert
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods
SEFM, 2005.

@proceedings{SEFM-2005,
	address       = "Koblenz, Germany",
	editor        = "Bernhard K. Aichernig and Bernhard Beckert",
	ee            = "http://www.computer.org/csdl/proceedings/sefm/2005/2435/00/index.html",
	isbn          = "0-7695-2435-4",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods}",
	year          = 2005,
}

Contents (45 items)

9 ×#verification
4 ×#analysis
4 ×#formal method
4 ×#framework
4 ×#using
3 ×#automaton
3 ×#composition
3 ×#invariant
3 ×#logic
3 ×#process

SEFM-2005-LeinenbachPP #code generation #compilation #implementation #towards #verification

Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes (DL, WJP, EP), pp. 2–12.

SEFM-2005-Trakhtenbrot #debugging #testing #using #verification

Use of Verification for Testing and Debugging of Complex Reactive Systems (MBT), pp. 13–22.

SEFM-2005-DorofeevaYEC #evaluation #testing

Experimental Evaluation of FSM-Based Testing Methods (RD, NY, KEF, ARC), pp. 23–32.

SEFM-2005-JhumkaH #detection

Putting Detectors in Their Place (AJ, MH), pp. 33–43.

SEFM-2005-LanotteMT #analysis #automaton #data type #design #distributed

Timed Automata with Data Structures for Distributed Systems Design and Analysis (RL, AMS, AT), pp. 44–53.

SEFM-2005-SunW #process #realtime #refinement #semantics

Operational Semantics for Real-Time Processes with Action Refinement (XS, JW), pp. 54–63.

SEFM-2005-GebremichaelV #automaton #specification

Specifying Urgency in Timed I/O Automata (BG, FWV), pp. 64–74.

SEFM-2005-Bjorner #re-engineering

A Cloverleaf of Software Engineering (DB), pp. 75–85.

SEFM-2005-BarthePS #analysis #logic #memory management #precise #using

Precise Analysis of Memory Consumption using Program Logics (GB, MP, GS), pp. 86–95.

SEFM-2005-SubramaniamS #protocol #using

Using Dominators to Extract Observable Protocol Contexts (MS, JS), pp. 96–105.

SEFM-2005-WandelerJLT #automaton #interface #modelling #static analysis

Counting Interface Automata and their Application in Static Analysis of Actor Models (EW, JWJ, EAL, LT), pp. 106–116.

SEFM-2005-GervaisFL #database #generative #recursion #relational #transaction

Generating Relational Database Transactions From Recursive Functions Defined on EB3 Traces (FG, MF, RL), pp. 117–126.

SEFM-2005-NemethPP #workflow

Workflow Enactment Based on a Chemical Metaphor (ZN, CP, TP), pp. 127–136.

SEFM-2005-JacobsPLS #concurrent #invariant

Safe Concurrency for Aggregate Objects with Invariants (BJ, FP, KRML, WS), pp. 137–147.

SEFM-2005-Leino #invariant

Invariants on Demand (KRML), pp. 148–149.

SEFM-2005-WilsonMC #approach #configuration management #flexibility #policy #verification

Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verification (TW, SM, RGC), pp. 150–159.

SEFM-2005-Trentelman #correctness #proving #using

Proving Correctness of JavaCard DL Taclets using Bali (KT), pp. 160–169.

SEFM-2005-GrandySR #java #kernel #object-oriented #verification

Object Oriented Verification Kernels for Secure Java Applications (HG, KS, WR), pp. 170–179.

SEFM-2005-OlssonW #correctness #imperative #induction #proving #source code

Customised Induction Rules for Proving Correctness of Imperative Programs (OO, AW), pp. 180–189.

SEFM-2005-HubertM #algorithm #c #case study #source code #verification

A case study of C source code verification: the Schorr-Waite algorithm (TH, CM), pp. 190–199.

SEFM-2005-BlechGG #higher-order #verification

Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.

SEFM-2005-NivelleP #verification

Verification of an Off-Line Checker for Priority Queues (HdN, RP), pp. 210–219.

SEFM-2005-PrasetyaAVL #composition #generative #verification

Building Verification Condition Generators by Compositional Extensions (ISWBP, AA, TEJV, AvL), pp. 220–230.

SEFM-2005-JinH #concurrent #process #towards

Towards A Truly Concurrent Model for Processes Sharing Resources (NJ, JH), pp. 231–239.

SEFM-2005-KuehnLE #petri net

A Proposal For Relative Time Petri Nets (JK, CL, RE), pp. 240–249.

SEFM-2005-SadaniSC #framework #petri net #platform #verification

From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform (TS, PdSS, JPC), pp. 250–260.

SEFM-2005-Hall #formal method

Making Formal Methods Work (AH), pp. 261–262.

SEFM-2005-PapCD #formal method #on the

On the Theory of Patching (ZP, GC, SD), pp. 263–271.

SEFM-2005-ScheffczykBBS #consistency #industrial #requirements #specification

Pragmatic Consistency Management in Industrial Requirements Specifications (JS, UMB, AB, JS), pp. 272–281.

SEFM-2005-WelchFD #automation #invariant #maintenance

Automatic Maintenance of Association Invariants (JW, DF, JD), pp. 282–292.

SEFM-2005-Sifakis #component #framework

A Framework for Component-based Construction Extended Abstract (JS), pp. 293–300.

SEFM-2005-PredaG #abstract interpretation #obfuscation

Control Code Obfuscation by Abstract Interpretation (MDP, RG), pp. 301–310.

SEFM-2005-NejatiGC #abstraction

Stuttering Abstraction for Model Checkin (SN, AG, MC), pp. 311–320.

SEFM-2005-GeorgievaM #analysis #logic

Description Logics for Shape Analysis (LG, PM), pp. 321–331.

SEFM-2005-ShiRB #formal method #robust

Formalising Control in Robust Spoken Dialogue Systems (HS, RJR, JAB), pp. 332–341.

SEFM-2005-DittmarF

A unified description formalism for complex HCI-systems (AD, PF), pp. 342–351.

SEFM-2005-CeroneLC #analysis #formal method #human-computer #interactive #model checking #using

Formal Analysis of Human-computer Interaction using Model-checking (AC, PAL, SC), pp. 352–362.

SEFM-2005-CarterMM #developer #refinement

Software Refinement with Perfect Developer (GC, RM, JMM), pp. 363–373.

SEFM-2005-ColinPPRMM #development #framework #open source #platform #xml

BRILLANT : An Open Source and XML-based platform for Rigourous Software Development (SC, DP, VP, JR, RM, GM), pp. 373–382.

SEFM-2005-Chalin #logic #question #what

Logical Foundations of Program Assertions: What do Practitioners Want? (PC), pp. 383–393.

SEFM-2005-Hameurlain #behaviour #component #on the #protocol

On Compatibility and Behavioural Substitutability of Component Protocols (NH), pp. 394–403.

SEFM-2005-MesquitaSM #composition #framework

A Strategy for the Formal Composition of Frameworks (WM, AS, ACVdM), pp. 404–413.

SEFM-2005-GurovH #abstraction #composition #interface

Interface Abstraction for Compositional Verificatio (DG, MH), pp. 414–424.

SEFM-2005-HirschT #coordination #named

SHReQ: Coordinating Application Level QoS (DH, ET), pp. 425–434.

SEFM-2005-AnantharamanCH #calculus #process

A Synchronous Process Calculus for Service Costs (SA, JC, GH), pp. 435–444.