Jeannette M. Wing, Jim Woodcock, Jim Davies
Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Volume I
World Congress on Formal Methods, 1999.
@proceedings{FM-v1-1999, address = "Toulouse, France", editor = "Jeannette M. Wing and Jim Woodcock and Jim Davies", isbn = "3-540-66587-0", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Volume I}", volume = 1708, year = 1999, }
Contents (50 items)
- FM-v1-1999-Hoare #bottom-up #programming #top-down
- Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle (CARH), pp. 1–27.
- FM-v1-1999-Jones
- Scientific Decisions which Characterize VDM (CBJ), pp. 28–47.
- FM-v1-1999-Rushby #formal method #question
- Mechanized Formal Methods: Where Next? (JMR), pp. 48–51.
- FM-v1-1999-Sifakis #integration
- Integration, the Price of Success (JS), pp. 52–55.
- FM-v1-1999-Jackson
- The Role of Formalism in Method (MJ), p. 56.
- FM-v1-1999-ConquetM #automation #design #testing
- Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project (EC, JLM), pp. 57–75.
- FM-v1-1999-EertinkJLTV #design #process
- A Business Process Design Language (HE, WJ, POL, WBT, CAV), pp. 76–95.
- FM-v1-1999-PhilippsR #architecture #refinement
- Refinement of Pipe-and-Filter Architectures (JP, BR), pp. 96–115.
- FM-v1-1999-HerbertDRS #architecture #formal method
- A Formalization of Software Architecture (JH, BD, RAR, VS), pp. 116–133.
- FM-v1-1999-Kurki-Suonio #component #interface #refinement #specification
- Component and Interface Refinement in Closed-System Specifications (RKS), pp. 134–154.
- FM-v1-1999-Pavlovic #first-order #parametricity #semantics #specification
- Semantics of First Order Parametric Specifications (DP), pp. 155–172.
- FM-v1-1999-KestenKPR #analysis #deduction #model checking #verification
- A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software (YK, AK, AP, GR), pp. 173–194.
- FM-v1-1999-ReffelE #detection #fault #model checking
- Error Detection with Directed Symbolic Model Checking (FR, SE), pp. 195–211.
- FM-v1-1999-AlurEKKL #analysis #case study #coordination #formal method #hybrid #modelling #multi
- Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination (RA, JME, MK, VK, IL), pp. 212–232.
- FM-v1-1999-TripakisA #on the fly #synthesis
- On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems (ST, KA), pp. 233–252.
- FM-v1-1999-Couvreur #linear #logic #on the fly #verification
- On-the-Fly Verification of Linear Temporal Logic (JMC), pp. 253–271.
- FM-v1-1999-DeharbeM #fixpoint #model checking
- Symbolic Model Checking with Fewer Fixpoint Computations (DD, AMM), pp. 272–288.
- FM-v1-1999-BarbutiFSV #abstraction #model checking #realtime
- Formula Based Abstractions of Transition Systems for Real-Time Model Checking (RB, NDF, AS, GV), pp. 289–306.
- FM-v1-1999-BozgaFGGKM #named #representation #validation
- IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems (MB, JCF, LG, SG, JPK, LM), pp. 307–327.
- FM-v1-1999-Wang #automation #pointer #process #verification
- Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes (FW), pp. 328–347.
- FM-v1-1999-SabatierL #design #formal method #smarttech #transaction #using #validation
- The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications (DS, PL), pp. 348–368.
- FM-v1-1999-BehmBFM #named #scalability
- Météor: A Successful Application of B in a Large Project (PB, PB, AF, JMM), pp. 369–387.
- FM-v1-1999-MatthewsL #database #development
- Formal Development of Databases in ASSO and B (BM, EL), pp. 388–410.
- FM-v1-1999-Rouzaud #calculus #refinement
- Interpreting the B-Method in the Refinement Calculus (YR), pp. 411–430.
- FM-v1-1999-BuchiB #composition #symmetry
- Compositional Symmetric Sharing in B (MB, RJB), pp. 431–451.
- FM-v1-1999-MunozR
- Structural Embeddings: Mechanization with Method (CAM, JMR), pp. 452–471.
- FM-v1-1999-Dunne #specification
- The Safe Machine: A New Specification Construct for B (SD), pp. 472–489.
- FM-v1-1999-Butler #approach #csp #named
- csp2B: A Practical Approach to Combining CSP and B (MJB), pp. 490–508.
- FM-v1-1999-Waeselynck #modelling
- Test Criteria Definition for B Models (SB, HW), pp. 509–529.
- FM-v1-1999-PaigeH #concurrent #object-oriented #realtime #specification
- Bunches for Object-Oriented, Concurrent, and Real-Time Specification (RFP, ECRH), pp. 530–550.
- FM-v1-1999-TyuguMP #source code #synthesis
- Applications of Structural Synthesis of Programs (ET, MM, JP), pp. 551–569.
- FM-v1-1999-CharpentierC #approach #composition #design #distributed #towards #verification
- Towards a Compositional Approach to the Design and Verification of Distributed Systems (MC, KMC), pp. 570–589.
- FM-v1-1999-WongC #case study #formal method #modelling
- Formal Modeling in a Commercial Setting: A Case Study (AW, MC), pp. 590–607.
- FM-v1-1999-BurdonovKPG #automation #generative #named #specification #testing
- KVEST: Automated Generation of Test Suites from Formal Specifications (IBB, AK, AP, DG), pp. 608–621.
- FM-v1-1999-Bousquet #case study #detection #experience #feature model #interactive #model checking #testing #using
- Feature Interaction Detection Using Testing and Model-Checking Experience Report (LdB), pp. 622–641.
- FM-v1-1999-HusbergM #industrial #named #reachability
- Emma: Developing an Industrial Reachability Analyser for SDL (NH, TM), pp. 642–661.
- FM-v1-1999-MoninK #algorithm #consistency #correctness #proving #standard
- Correctness Proof of the Standardized Algorithm for ABR Conformance (JFM, FK), pp. 662–681.
- FM-v1-1999-ArtsD #database #distributed #erlang #verification
- Verifying a Distributed Database Lookup Manager Written in Erlang (TA, MD), pp. 682–700.
- FM-v1-1999-GilhamRS #database #distributed
- Secure Interoperation of Secure Distributed Databases (FG, RAR, VS), pp. 701–717.
- FM-v1-1999-LotzKW #hardware #security
- A Formal Security Model for Microprocessor Hardware (VL, VK, GW), pp. 718–737.
- FM-v1-1999-Schneider #abstraction #testing
- Abstraction and Testing (SS), pp. 738–757.
- FM-v1-1999-ZhouC #analysis #communication #formal method #protocol
- Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol (DZ, SKC), pp. 758–775.
- FM-v1-1999-LincolnMMS #analysis #equivalence #polynomial #probability #security
- Probabilistic Polynomial-Time Equivalence and Security Analysis (PL, JCM, MM, AS), pp. 776–793.
- FM-v1-1999-FocardiM #approach #security
- A Uniform Approach for the Definition of Security Properties (RF, FM), pp. 794–813.
- FM-v1-1999-SyversonS #formal method
- Group Principals and the Formalization of Anonymity (PFS, SGS), pp. 814–833.
- FM-v1-1999-PaigeO #formal method
- Developing BON as an Industrial-Strength Formal Method (RFP, JSO), pp. 834–853.
- FM-v1-1999-MandelC #ocl #on the #power of
- On the Expressive Power of OCL (LM, MVC), pp. 854–874.
- FM-v1-1999-MeyerS #approach #diagrams #specification
- A Systematic Approach to Transform OMT Diagrams to a B Specification (EM, JS), pp. 875–895.
- FM-v1-1999-Liu #consistency #specification #testing #verification
- Verifying Consistency and Validity of Formal Specifications by Testing (SL), pp. 896–914.
- FM-v1-1999-TabourierCI #empirical #protocol #testing #using
- A GSM-MAP Protocol Experiment Using Passive Testing (MT, ARC, MI), pp. 915–934.
8 ×#formal method
7 ×#specification
6 ×#testing
6 ×#verification
5 ×#model checking
5 ×#named
4 ×#analysis
4 ×#approach
4 ×#design
3 ×#automation
7 ×#specification
6 ×#testing
6 ×#verification
5 ×#model checking
5 ×#named
4 ×#analysis
4 ×#approach
4 ×#design
3 ×#automation