|
What's New on the VASY Web Server? |
This is the list of the most recent pages on the VASY Web server:
See also our (regularly updated) Publication Page.
VASY Press Releases
2011
Aerospace: better, faster and less costly design (French or English)
Hubert Garavel receives the Gay-Lussac Humboldt Research Award (French or English)
Other Additions to the VASY Web Site:
- Jan. 2011: Towards Performance Prediction of Compositional Models in GALS Designs
- Jan 2011: Modélisation et analyse des performances de la bibliothèque MPI en tenant compte de l'architecture matérielle
- Jan. 2011: A Study of Shared-Memory Mutual Exclusion Protocols using CADP
- Jan. 2011: Slides of W. Serwe's lecture at FMICS 2010
- Jan. 2011: Translating Pi-Calculus into LOTOS NT
- Jan. 2011: Slides of G. Salaün's lecture IFM 2010
- Jan 2011: Ten Years of Performance Evaluation for Concurrent Systems Using CADP
- Jan. 2011: Slides of F. Lang's lecture at ISoLA 2010
- Jan. 2011: Translating FSP into LOTOS and Networks of Automata
- Mar. 2011: Academic and Professional Training using CADP (2009-2010 Update)
- Mar. 2011: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
- Mar. 2011: Smart Reduction
- Mar. 2011: Measuring the Compatibility of Service Interaction Protocols
- Mar. 2011: [CADP-based tool] TEPAWSN Environment for the Design of Wireless Sensor Networks
- Mar. 2011: [CADP-based tool] LTSmin Toolset for Manipulating LTSs
- Mar. 2011: [CADP-based tool] Alvis Modelling Language for Embedded Systems
- Mar. 2011: [CADP-based tool] JTorX Tool for Model-Based Testing of Software
- Mar. 2011: [CADP-based tool] Argos Tool for Analysing UML Descriptions
- Mar. 2011: [CADP-based tool] Henshin Language and Toolset for Transformation of Eclipse Models
- Mar. 2011: [CADP case study] Workflow specification using LOTOS
- Mar. 2011: [CADP case study] Multilateral and RBAC Security for Management of Distributed Systems
- Mar. 2011: [CADP case study] Learnlib Framework for Extrapolating Behavioral Models
- Mar. 2011: [CADP case study] Evaluation of Packet Latency on a 2D Mesh Network-on-Chip
- Mar. 2011: [CADP case study] Specification and Verification of Hardware Circuits
- Mar. 2011: [CADP case study] Automated Formal Analysis of CRESS Web and Grid Services
- Mar. 2011: [CADP case study] Model-Checking Erlang
- Mar. 2011: [CADP case study] Translation Validation of (Multi-Clocked) SIGNAL Specifications
- Mar. 2011: [CADP case study] Verification of Web Service Composition
- Mar. 2011: [CADP case study] Systematic Correct Construction of Self-Stabilizing Systems
- Mar. 2011: [CADP case study] Verification of the Behavioural Properties for Group Communications
- Mar. 2011: [CADP case study] Mutual Exclusion Protocols
- Mar. 2011: MULTIVAL Progress Report 2010 by the VASY project-team of INRIA
- Mar. 2011: [new CADP tool] EVALUATOR 4.0 model checker for MCL temporal logic formulas
- Apr. 2011: [new CADP tool] PBG_RM tool
- Apr. 2011: [new CADP tool] PBG_INFO tool
- Apr. 2011: [new CADP tool] PBG_CP tool
- Apr. 2011: [new CADP tool] PBG_MV tool
- May 2011: Slides of F. Lang's lecture at FASE 2011
- May 2011: Slides of D. Thivolle's PhD defense
- Jun. 2011: VASY is seeking a post-doctoral scientist (job #2011A)
- Jun. 2011: STMicroelectronics and VASY are seeking a PhD student (job #2011B)
- Jul. 2011: CTRL: Extension of CTL with Regular Expressions and Fairness Operators to Verify Genetic Regulatory Networks
- Jul. 2011: Property-Dependent Reductions for the Modal Mu-Calculus
2010
Other Additions to the VASY Web Site:
- Jan. 2010: [new CADP tool] LPP: LOTOS / LOTOS NT pre-processor
- Jan. 2010: [new CADP tool] LNT2LOTOS: LOTOS NT to LOTOS translator
- Jan. 2010: [new CADP tool] LNT.OPEN: OPEN/CAESAR connection for the LOTOS NT language
- Feb. 2010: A Service-Oriented Architecture for Integrating the Modeling and Formal Verification of Genetic Regulatory Networks
- Feb. 2010: TLM.OPEN: a SystemC/TLM Front-End for the CADP Verification Toolbox
- Feb. 2010: Towards Performance Prediction of Compositional Models in Industrial GALS Designs
- Feb. 2010: Slides of N. Coste's lecture at CAV'09
- Feb. 2010: VASY and Bull are seeking a PhD student (job #2010A)
- Feb. 2010: VASY is seeking a software engineer (job #2010B)
- Mar. 2010: Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.0)
- Mar. 2010: [CADP case study] Model Based Importance Analysis for Minimal Cut Sets
- Mar. 2010: [CADP case study] Formal Verification of ToolBus Scripts
- Mar. 2010: [CADP case study] Gossiping Networks
- Mar. 2010: [CADP case study] Collaboration Diagrams
- Mar. 2010: [CADP case study] Verification of a Turntable System
- Mar. 2010: [CADP case study] Validation of Semantic Composability in Simulation Models
- Mar. 2010: [CADP case study] Formal Analysis of Consensus Protocols
- Mar. 2010: [CADP case study] Accelerated Heartbeat Protocols
- Mar. 2010: [CADP case study] Dependability and Survivability Evaluation of a Water Distribution Process
- Mar. 2010: [CADP case study] Blitter Display
- Mar. 2010: [CADP case study] Trivial File Transfer Protocol
- Mar. 2010: [CADP case study] Performance Evaluation of MPI on CC-NUMA Architectures
- Mar. 2010: [CADP case study] Test Generation for Automotive Industry
- Mar. 2010: [CADP-based tool] ITACA/ACIDE Toolbox for Composition and Adaptation of Web Services
- Mar. 2010: [CADP-based tool] FLORA Framework for Software Architectures with Local Recovery
- Mar. 2010: [CADP-based tool] AVATR Tool for Analyzing Test Results of Océ Printers
- Mar. 2010: [CADP-based tool] Performance Evaluation of Distributed Systems Based on Process Algebras
- May 2010: Asynchrony in embedded systems: the Multival project (slides of H. Garavel's lecture at ESE'09)
- May 2010: [CADP case study] Equipment Failure Management Protocol
- May 2010: [CADP case study] Air Traffic Control Subsystem
- Dec 2010: MULTIVAL Progress Report 2009 by the VASY project-team of INRIA
2009
Other Additions to the VASY Web Site:
- Jan. 2009: Claude Helmstetter's Home Page
- Jan. 2009: Is Timed Branching Bisimilarity a Congruence Indeed?
- Mar. 2009: [CADP case study] Abstraction and Analysis of Clinical Guidance Trees
- Apr. 2009: [CADP case study] Verification of Distributed Shared Memory Systems
- Apr. 2009: [CADP case study] Leader Election in Anonymous Ring
- Apr. 2009: [CADP case study] Analysis of First-Class Futures of Distributed Grid Components
- Apr. 2009: [CADP case study] Verification and Adaptation of WF/.NET Components
- Apr. 2009: [CADP case study] Specification and Verification of Middlewares
- Apr. 2009: [CADP case study] Performance Analysis of Stimulus Rich Reactive Interfaces
- May 2009: MULTIVAL Progress Report 2008 by the VASY project-team of INRIA
- Jun. 2009: xSTream : Architecture multi-coeur sur puce pour des applications multimédia
- Jun. 2009: [CADP case study] Specification and Analysis of a Web Service for GPS Navigation
- Jun. 2009: [CADP-based tool] Contracts and Protocols for Web Services
- Jun. 2009: [CADP-based tool] SynthesisRT: Adaptors for Real-Time Components
- Jun. 2009: [CADP-based tool] Transformation, Analysis and Validation of MODEST Models
- Jun. 2009: [CADP-based tool] CORAL (COmpositional Reliability and Availability anaLysis)
- Jun. 2009: [CADP-based tool] Enhanced version of the ETI: Service Based Coordination of Heterogeneous Tools
- Jun. 2009: [CADP-based tool] Enhanced version of the CRESS tool: Analysis of Composed Grid Services
- Jun. 2009: [CADP-based tool] CTTool for Analyzing Fractal/GCM Components with UML 2
- Jun. 2009: [CADP-based tool] DATALOG_SOLVE Tool for Static Analysis of Object-Oriented Programs
- Jun. 2009: [CADP-based tool] COSTO Tool for Analyzing Kmelia Components and Services
- Jul. 2009: Revised BCG_WRITE manual page
- Jul. 2009: Revised BCG_READ manual page
- Jul. 2009: [new CADP tool] FSP.OPEN: OPEN/CAESAR connection for the FSP language
- Jul. 2009: Les résultats du projet OpenEmbeDD
- Jul. 2009: Survey on Directed Model Checking
- Jul. 2009: Modeling Multiprocessor Cache Protocol Impact on MPI Performance
- Jul. 2009: [new CADP tool] CUNCTATOR: on-the-fly steady-state simulation of continuous-time Markov chains
- Jul. 2009: Intermediate Models for the Verification of Asynchronous Real-Time Embedded Systems
- Jul. 2009: Model Checking of Action-Based Concurrent Systems
- Jul. 2009: Formal Modeling and Discrete-Time Analysis of BPEL Web Services
- Jul. 2009: Hierarchical Adaptive State Space Caching based on Level Sampling
- Jul. 2009: Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format
- Jul. 2009: [new CADP tool] CONTRIBUTOR: CADP contribution assistant
- Aug. 2009: VASY is seeking a software engineer (job #2009C)
- Aug. 2009: VASY is seeking a software engineer (job #2009D)
- Sep. 2009 [CADP-based tool] Automatic Generation of Interfaces for Model Checking
- Sep. 2009 [CADP-based tool] CHARMY and SYNTHESIS Tools for Analyzing Software Architectures
- Sep. 2009 [CADP-based tool] ARCADE Tool for Analyzing Input/Output Interactive Markov Chains
- Sep. 2009 [CADP-based tool] DCOMPOSITOR Tool for Generating Service Wrapper Protocols
- Sep. 2009 [CADP-based tool] Tool for Random Exploration and Testing
- Sep. 2009 [CADP-based tool] Tool for Performance Evaluation and Functional Verification in Stochastic Process Algebras
- Sep. 2009: VASY is seeking a software engineer (job #2009E)
- Oct. 2009: VASY and Bull are seeking a PhD student (job #2009F)
- Nov. 2009: Slides of O. Ponsini's lecture at FM'08
- Nov. 2009: Slides of O. Ponsini's lecture at MEMOCODE'08
- Nov. 2009: Slides of Cl. Helmstetter's lecture at MEMOCODE'09
- Dec. 2009: On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP
- Dec. 2009: Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
- Dec. 2009: Verification of an Industrial SystemC/TLM Model using LOTOS and CADP
- Dec. 2009: Efficient On-the-Fly Computation of Weak Tau-Confluence
- Dec. 2009: Extending SPARQL with Temporal Logic
- Dec. 2009: Partial Order Reductions using Compositional Confluence Detection
2008
Other Additions to the VASY Web Site:
- Jan. 2008: Anton Wijs's Home Page
- Jan. 2008: FormalFame 2007 Activity Report
- Feb. 2008: MULTIVAL Progress Report 2007 by the VASY project-team of INRIA
- Feb. 2008: [CADP case study] Verification of a .Net On-Line Sale Application
- Feb. 2008: [CADP case study] Verification of Adaptors between Evolving Components
- Mar. 2008: Vérification formelle de systèmes et circuits asynchrones - Collaboration IAN-VASY
- Mar. 2008: Slides of N. Coste's lecture at DATE'08
- Mar. 2008: FIACRE: An Intermediate Language for Model Verification in the TopCased Environment
- Mar. 2008: A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS
- Mar. 2008: [CADP case study] Chaum's dining cryptographers and Fujioka-Okamota-Ohta electronic voting scheme
- Mar. 2008: [CADP case study] Formal Analysis of Erlang's Open Telecom Platform Library Components
- Mar. 2008: [CADP case study] Bridge Exchanger Software Connectors for Dataflow Applications
- Mar. 2008: [CADP case study] Automatic Verification of the IEEE 1394 Tree Identify Protocol
- Mar. 2008: [CADP case study] Verification of the Dutch Rijnland Internet Election System
- Mar. 2008: [CADP case study] Analysis of Wireless Sensor Network Applications for TinyOS
- Mar. 2008: [CADP case study] Model-Based Testing of Registrar Entity for the Session Initiation Protocol
- Apr. 2008: A Comparison of Two SystemC/TLM Semantics for Formal Verification
- May 2008: Performance Evaluation of MPI Benchmarks on CC-DSM Multiprocessor Architectures (Slides of M. Zidouni's lecture at MODEL35)
- Jun. 2008: Séminaire VASY 2008
- Jul. 2008: VASY is seeking a software engineer (job #2008A)
- Jul. 2008: VASY is seeking a software engineer (job #2008B)
- Jul. 2008: [CADP-based tool] Abstract Test Case Execution Framework
- Jul. 2008: [CADP-based tool] Interoperability Test Generation Algorithm
- Jul. 2008: [CADP-based tool] LYS Knowledge Analysis Toolset for Epistemic Verification
- Sep. 2008: Specification and Analysis of Asynchronous Systems using CADP
- Sep. 2008: A Model Checking Language for Concurrent Value-Passing Systems
- Sep. 2008: Slides of D. Thivolle's lecture at FM'08
- Oct. 2008: Recent scientific publications using the VLTS benchmark suite
- Oct. 2008: Verifying Dynamic Properties of Industrial Critical Systems Using TOPCASED/FIACRE
- Dec. 2008: Computation Tree Regular Logic for Genetic Regulatory Networks
- Dec. 2008: Slides of R. Mateescu describing the Computation Tree Regular Logic
- Dec. 2008: Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems
- Dec. 2008: Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques
- Dec. 2008: Formal Modeling and Discrete-Time Analysis of BPEL Web Services
- Dec. 2008: [new CADP tool] FSP to LOTOS translator
- Dec. 2008: Improved On-the-Fly Equivalence Checking using Boolean Equation Systems
- Dec. 2008: Slides of E. Oudot's lecture at SPIN'08
- Dec. 2008: Temporal Logic Patterns for Querying Qualitative Models of Genetic Regulatory Networks
- Dec. 2008: Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks
- Dec. 2008: Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks
- Dec. 2008: VASY is seeking a software engineer (job #2008C)
- Dec. 2008: VASY is seeking a software engineer (job #2008D)
- Dec. 2008: VASY is seeking a technical writer (job #2008E)
2007
CADP 2006: Modelling and checking asynchronous systems (French or English)
(Positive) Evaluation of the VASY team (2003-2007) (Restricted access)
Other Additions to the VASY Web Site:
- Jan. 2007: Refined interfaces for compositional verification (Extended slides of F. Lang's lecture at FORTE'06)
- Jan. 2007: VASY is seeking a software engineer (job #2007A)
- Apr. 2007: Olivier Ponsini's Home Page
- Apr. 2007: VASY is seeking a performance evaluation expert (job #2007B)
- Jun. 2007: FormalFame 2005 Activity Report
- Jun. 2007: FormalFame 2006 Activity Report
- Jul. 2007: The VASY Team (slides of H. Garavel for INRIA ComC quadrennial evaluation)
- Jul. 2007: Translating FSP into LOTOS and Networks of Automata (slides of G. Salaün at IFM'2007)
- Jul. 2007: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes (slides of H. Garavel at CAV'2007)
- Jul. 2007: Le projet MULTIVAL (slides of H. Garavel at the OPEES workshop)
- Jul. 2007: VASY is seeking a software engineer (job #2007C)
- Jul. 2007: VASY is seeking a software engineer (job #2007D)
- Jul. 2007: Translating FSP into LOTOS and Networks of Automata
- Oct. 2007: Le langage pivot asynchrone FIACRE (slides of F. Lang)
- Oct. 2007: CADP Twenty Years After (slides of H. Garavel at the IFIP WG1.8 workshop)
- Oct. 2007: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
- Oct. 2007: Formal Verification of CHP Specifications with CADP - Illustration on an Asynchronous Network-on-Chip
- Nov. 2007: [new CADP tool] BES_SOLVE
- Nov. 2007: Behavioral Adaptation of Component Compositions based on Process Algebra Encodings
- Dec. 2007: Emilie Oudot's Home Page
- Dec. 2007: [CADP case study] Verification of an Asynchronous Network-on-Chip
- Dec. 2007: Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular
- Dec. 2007: Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures
2006
Evaluation of the VASY team as part of the LIG laboratory (March 2006) (Restricted access)
Minalogic/MULTIVAL: Validation of Multiprocessor Multithreaded Architectures
Other Additions to the VASY Web Site:
- Jan. 2006: DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation
- Jan. 2006: [CADP case study] Testing of Electron Beam Accelerators for Radiotherapy
- Jan. 2006: [CADP case study] Constraint Solving with LOTOS
- Jan. 2006: [CADP case study] Verification of a Fair Non-Repudiation Protocol
- Jan. 2006: [CADP case study] Verification of Fractal Components
- Jan. 2006: The VASY Team (slides of H. Garavel for LIG laboratory evaluation)
- Mar. 2006: [new CADP tool] REDUCTOR V5
- Mar. 2006: Vérification distribuée à la volée de grands espaces d´états
- Mar. 2006: [new CADP demo] Web services for stock management and on-line book auctions
- Mar. 2006: VASY is seeking a PhD candidate (job #2006A)
- Mar. 2006: VASY is seeking a post-doc candidate (job #2006B)
- Apr. 2006: SENVA Scientific Report 2005
- Apr. 2006: SENVA Meeting on Parallel and Distributed Verification
- Apr. 2006: Fully-redesigned CADP Publication Page
- Apr. 2006: Slides of R. Mateescu's lecture at TACAS'06
- Apr. 2006: Distributed On-the-Fly Model Checking and Test Case Generation
- Apr. 2006: Slides of R. Mateescu's lecture at SPIN'06
- Apr. 2006: VASY is seeking a software engineer (job #2006C)
- Jun. 2006: SENVA 2006 Workshop
- Jun. 2006: ST Microelectronics and VASY are seeking a PhD candidate (job #2006D)
- Jun. 2006: VASY is seeking a post-doc candidate (job #2006E)
- Jun. 2006: VASY is seeking a software engineer (job #2006F)
- Jun. 2006: Bull and VASY are seeking a PhD candidate (job #2006G)
- Jul. 2006: VASY is seeking a software engineer (job #2006H)
- Jul. 2006: Bounded Analysis and Decomposition for Behavioural Descriptions of Components
- Jul. 2006: Synchronizing Behavioural Mismatch in Software Composition
- Jul. 2006: Slides of G. Salaün's lecture at FMOODS'06
- Jul. 2006: CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems
- Jul. 2006: CADP Tools Overview (updated)
- Sep. 2006: [CADP case study] Verification of Software Components
- Oct. 2006: [CADP case study] Automatic Document Feeder
- Oct. 2006: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
- Oct. 2006: Modélisation et analyse de systèmes asynchrones avec CADP
- Oct. 2006: VASY is seeking a software engineer (job #2006I)
- Oct. 2006: VASY is seeking a software engineer (job #2006J)
- Oct. 2006: Refined Interfaces for Compositional Verification
- Dec. 2006: SENVA Scientific Report 2006
- Dec. 2006: The SENVA Joint Team
- Dec. 2006: CADP 2006 from a Model Driven Perspective
- Dec. 2006: [CADP case study] Transport Layer Security Protocol
- Dec. 2006: [CADP case study] Fault-Based Testing of Concurrent Systems
- Dec. 2006: [CADP case study] Verifying Fault-Tolerant Erlang Programs
- Dec. 2006: [CADP case study] Formal Specification and Verification of a DRM Protocol
- Dec. 2006: [CADP case study] Verification of Observational Determinism
- Dec. 2006: [CADP case study] Performability Evaluation of the European Train Control System
- Dec. 2006: [CADP-based tool] Model-Based Software Adaptation
- Dec. 2006: [CADP-based tool] Verification of Real-Time Systems
- Dec. 2006: [CADP-based tool] ANNOTATOR Tool for On-the-Fly Data Flow Analysis
- Dec. 2006: [CADP-based tool] Software Model Checking
- Dec. 2006: [CADP-based tool] Vercors Platform for Model Checking Distributed Components
- Dec. 2006: VASY is seeking a post-doc candidate (job #2006K)
2005
Other Additions to the VASY Web Site:
- Jan. 2005: The SENVA Collaboration
- Jan. 2005: SENVA Scientific Report 2004
- Jan. 2005: Dr. Jaco van de Pol is appointed Group Leader of SEN2
- Jan. 2005: [new CADP tool]: DISTRIBUTOR
- Feb. 2005: Scientific publications mentioning the VLTS benchmark suite
- Feb. 2005: Distributed Local Resolution of Boolean Equation Systems
- Feb. 2005: Slides of Ch. Joubert's lecture at PDP'05
- Feb. 2005: [CADP-based tool] On-the-Fly Interconnection of CADP and mCRL Toolsets
- Feb. 2005: [new CADP demo] SCSI-2 bus arbitration protocol
- Feb. 2005: [new CADP demo] Computer integrated manufacturing
- Mar. 2005: [CADP-based tool] Model Checking Genetic Regulatory Networks using GNA and CADP
- Mar. 2005: VASY is seeking a post-doc candidate (job #2005A)
- Mar. 2005: VASY is seeking a post-doc candidate (job #2005B)
- Mar. 2005: [new CADP demo] Distributed summation algorithm
- Mar. 2005: [new CADP demo] Distributed Erathostenes sieve
- Apr. 2005: [CADP-based tool] Abstract Interpretation Toolkit for mCRL
- Apr. 2005: [CADP-based tool] Verification and Simulation of TURTLE (Real-Time UML) Diagrams
- Apr. 2005: Christophe Joubert's Home Page
- Apr. 2005: Combining functional verification and performance evaluation using CADP (cumulated slides by H. Garavel et al.)
- May 2005: Comparison between Caesar and the mcrl toolset - A response to Prof. Jan Friso Groote
- May 2005: BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
- Jun. 2005: SENVA 2005 Workshop
- Jun. 2005: Rapport d'activité FormalFame 2004
- Jul. 2005: Projet de Master 2 (protocole d'auto-réparation pour serveurs J2EE)
- Jul. 2005: Projet de Master 2 (vérification compositionnelle de systèmes embarqués)
- Jul. 2005: Etude de l'environnement ouvert de developpement intégré Eclipse dans l'optique d'une extension
- Jul. 2005: Projet de Master 2 (contraintes d'environnement pour la vérification énumérative)
- Jul. 2005: Projet de Master 2 (analyses statiques pour la réduction d'espace d'états)
- Sep. 2005: EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods
- Sep. 2005: Translating Hardware Process Algebras into Standard Process Algebras - Illustration with CHP and LOTOS
- Sep. 2005: [new CADP demo] ODP trader
- Sep. 2005: [new CADP demo] Asynchronous DES implementation
- Sep. 2005: [new CADP demo] Turntable system for drilling products
- Oct. 2005: How Formal Methods Can Contribute to the Formal Development of Web Services (cumulated slides by G. Salaün)
- Oct. 2005: Vérification de systèmes asynchrones avec CADP (slides by R. Mateescu)
- Oct. 2005: Encoding Abstract Descriptions into Executable Web Services: Towards a Formal Development
- Oct. 2005: [CADP case study] Automatic Verification of the IEEE 1394 Root Contention Protocol
- Oct. 2005: [CADP case study] Verification of the Chilean Electronic Invoices System
- Oct. 2005: [CADP case study] Formalising Middleware Behaviour using LOTOS
- Oct. 2005: [CADP case study] Formal Verification of a Fair Payment Protocol
- Oct. 2005: [CADP case study] Negotiation among Web Services using LOTOS/CADP
- Oct. 2005: [CADP case study] Reliable Large Scale Multipoint Transport Protocol
- Oct. 2005: [CADP case study] Analysis of a Turntable System
- Nov. 2005 Analysis and Verification of Qualitative Models of Genetic Regulatory Networks: A Model-Checking Approach
- Nov. 2005: [new CADP tool]: REDUCTOR V4
- Dec. 2005: Slides of G. Salaün's lecture at IFM'05
- Dec. 2005: Slides of F. Lang's lecture at IFM'05
- Dec. 2005: [CADP case study] Formal Verification of the STBus Interconnect
- Dec. 2005 Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli
- Dec. 2005: On-the-Fly State Space Reductions for Weak Equivalences
2004
Other Additions to the VASY Web Site:
- Jan. 2004: Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones
- Jan. 2004: FormalFame 2003 Activity Report
- Jan. 2004: [CADP case study] Positive Acknowledgement Retransmission (PAR) Protocol
- Jan. 2004: [CADP case study] Jackal Distributed Shared Memory Implementation of Java
- Jan. 2004: [CADP case study] Distributed Data Space Architectures Described in Space Calculus
- Jan. 2004: [CADP case study] Parallel Programs Developed using JavaSpacesTM
- Jan. 2004: Analyse et vérification automatique de systèmes asynchrones (slides by H. Garavel, in French)
- Feb. 2004: SEQ.OPEN: A Tool for Efficient Trace-Based Verification
- Feb. 2004: Model Checking Genetic Regulatory Networks using GNA and CADP
- Feb. 2004: VASY is seeking a post-doc candidate
- Mar. 2004: [CADP case study] Compositional Verification of the ScalAgent Deployment Protocol
- Mar. 2004: [CADP case study] Agent-Based Dynamic Online Auction Protocol
- Mar. 2004: [CADP case study] Robot Teleoperation Architecture
- Mar. 2004: [CADP case study] Pragmatic General Multicast (PGM) Protocol
- Mar. 2004: [CADP case study] Asynchronous Circuit for Data Encryption Standard (DES)
- Mar. 2004: [CADP-based tool] Model Checking for Systems on Chip (SoC)
- Mar. 2004: [CADP-based tool] Verification of Real-Time Systems using ELSE and CADP
- Mar. 2004: [CADP-based tool] Analysis of VoiceXML Interactive Voice Services
- May 2004: Almost Ten Years of Process Algebras and Model Checking for Multiprocessor Architectures (slides by H. Garavel)
- May 2004: Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs
- May 2004: Model Checking for Software Architectures
- Jun. 2004: SENVA 2004 Workshop
- Jun. 2004: [new CADP demo] Distributed, lazy cache memory preserving sequential consistency
- Jun. 2004: [new CADP demo] Randomized binary distributed consensus protocol
- Jul. 2004: New Version of the CADP Web Site
- Jul. 2004: [new CADP tool]: CAESAR.BDD
- Aug. 2004: [new CADP tool]: EXP.OPEN version 2
- Nov. 2004: Gwen Salaün's Home Page
- Dec. 2004: [new CADP tool]: BCG_STEADY
- Dec. 2004: [new CADP tool]: BCG_TRANSIENT
- Dec. 2004: [new CADP tool]: DETERMINATOR
- Dec. 2004: [new CADP tool]: PROJECTOR version 2
- Dec. 2004: [new CADP tool]: BISIMULATOR
- Dec. 2004: [new CADP tool]: BCG_MERGE
- Dec. 2004: Distributed On-the-Fly Equivalence Checking
- Dec. 2004: Slides of Ch. Joubert's lecture at PDMC'04
- Dec. 2004: ArchWare: Architecting Evolvable Software
- Dec. 2004: State Space Reduction for Process Algebra Specifications
- Dec. 2004: [new CADP demo] Hubble space telescope lifetime
2003
TACAS 2003: 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems
(Positive) Evaluation of the VASY team (1999-2003) (Restricted access)
The VLTS Benchmark Suite - A joint project of CWI/SEN2 and INRIA/VASY
Other Additions to the VASY Web Site:
- Jan. 2003: A Set of Performance and Dependability Analysis Components for CADP
- Jan. 2003: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
- Feb. 2003: Aurore Collomb's Home Page
- Mar. 2003: Wendelin Serwe's Home Page
- Mar. 2003: The VASY Team (slides of H. Garavel for INRIA 1C quadrennial evaluation)
- Apr. 2003: Rapport d'activité FormalFame 2002
- Apr. 2003: Slides of R. Mateescu's lecture at DAIS'01
- Apr. 2003: Slides of H. Garavel's lecture at SPIN'01
- Apr. 2003: Slides of R. Mateescu's lecture at TACAS'02
- Apr. 2003: Slides of H. Hermanns's and Ch. Joubert's lecture at TACAS'03
- Apr. 2003: Slides of R. Mateescu presented at TACAS'03
- Apr. 2003: [CADP case study] AIDA (Automatic In-Flight Data Acquisition) System
- Apr. 2003: [CADP case study] JavaSpaces Shared Data Space Architecture
- Apr. 2003: Slides of F. Lang's lecture at CC'02
- May 2003: Cumulated slides about SVL by H. Garavel and F. Lang
- May 2003: Slides of H. Garavel lecture at the 2nd COST 247 workshop
- May 2003: [CADP case study] Needham-Schroeder Public Key Authentication Protocol
- May 2003: [CADP case study] Replication Features of the Splice Architecture
- May 2003: [CADP case study] Non-Refinement Transformations of Software Architectures
- May 2003: [CADP case study] SCSI-2 Bus Arbitration Protocol
- May 2003: [CADP case study] Object Modelling of Interactive Systems using UMLi
- May 2003: Academic and Professional Training using the CADP Toolset
- May 2003: Cumulated slides about NTIF by H. Garavel and F. Lang (in English)
- May 2003: Cumulated slides about NTIF by H. Garavel and F. Lang (in French)
- May 2003: On-the-Fly Verification using CADP
- May 2003: [CADP-based tool] Deriving Global Properties from Local Restrictions
- May 2003: [CADP-based tool] Analysis of Real-Time Systems Described in RT-LOTOS
- Jun. 2003: Tutorial on Action-Based Temporal Logics by R. Mateescu (in French)
- Jun. 2003: Cumulated slides about EVALUATOR 3.0 by R. Mateescu
- Jun. 2003: Cumulated slides about CAESAR_SOLVE by R. Mateescu (in French)
- Jun. 2003: Séminaire VASY 2003
- Jul. 2003: [CADP-based tool] High-level language and development environment for CAN control systems
- Sep. 2003: Calculating Tau-Confluence Compositionally
- Sep. 2003: Défense et illustration des algèbres de processus
- Sep. 2003: [new CADP tool]: BCG_GRAPH
- Oct 2003: Tutorials for CADP and LOTOS
- Oct 2003: Modocop Workshop on Smart Card Specification, Verification, and Testing
- Dec. 2003: Distributed Model Checking: From Abstract Algorithms to Concrete Implementations
- Dec. 2003: Compositional Verification using CADP of the ScalAgent Deployment Protocol for Software Components
- Dec. 2003: An overview of CADP 2001 (cumulated slides by H. Garavel, in English)
- Dec. 2003: Panorama de CADP 2001 (cumulated slides by H. Garavel, in French)
2002
Other Additions to the VASY Web Site:
- Jan. 2002: [CADP case study] Development of a Verified Erlang Program for Resource Locking
- Jan. 2002: [CADP case study] Analysis of a Distributed System for Lifting Trucks
- Jan. 2002: [CADP case study] Dynamic Reconfiguration Protocol for Agent-Based Applications
- Jan. 2002: [CADP case study] Formal Analysis of Checkpointing Algorithms
- Jan. 2002: [CADP case study] The Accounting Model of the TINA Architecture
- Jan. 2002: [CADP-based tool] Implementation of the FULL logic using XTL
- Jan. 2002: Revised version of paper "Parallel State Space Construction for Model-Checking"
- Jan. 2002: An Overview of CADP 2001
- Jan. 2002: Compositional Verification using SVL Scripts
- Jan. 2002: Compiler Construction using LOTOS NT
- Feb. 2002: Rapport d'activité Dyade/FormalFame 2001
- Feb. 2002: Rapport d'activité Dyade/FormalCard 2001
- Feb. 2002: Online form for job application at VASY
- Apr. 2002: Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
- May 2002: Vérification de circuits : problèmes et solutions - Exemple de TestBuilder
- May 2002: An Embedded Language Framework for Hardware Compilation
- May 2002: SPeeDI - a Verification Tool for Polygonal Hybrid Systems
- Jul. 2002: On Combining Functional Verification and Performance Evaluation using CADP
- Jul. 2002: VASY is seeking a software engineer (1/2)
- Jul. 2002: VASY is seeking a software engineer (2/2)
- Sep. 2002: Parallel and Distributed Model Checking (slides of H. Garavel's lecture at SFM'02:MC)
- Oct. 2002: [new CADP tool]: SEQ.OPEN
- Oct. 2002: On Combining Functional Verification and Performance Evaluation using CADP (slides of H. Hermanns's lecture at FME'02)
- Oct. 2002: 8th ERCIM FMICS Workshop (Trondheim, Norway) June 5-7, 2003
- Oct. 2002: Séminaire VASY 2002
- Nov. 2002: David Champelovier's Home Page
- Nov. 2002: Poster about the industrial usage of Evaluator 3.0
- Nov. 2002: A user's introduction to the CADP tools (French)
- Dec. 2002: NTIF: A General Symbolic Model for Communicating Sequential Processes with Data
- Dec. 2002: List of accepted research papers and tool demos at TACAS 2003
2001
Other Additions to the VASY Web Site:
- Jan. 2001: [CADP case study] LOTOS Patterns for Architectural Styles
- Jan. 2001: [CADP case study] SPLICE Coordination Architecture
- Jan. 2001: [CADP case study] Steam-Boiler System
- Jan. 2001: [CADP case study] POLYKID CC-NUMA Multiprocessor Architecture
- Jan. 2001: [CADP case study] Pipe & Filter Software Architectures
- Jan. 2001: [CADP case study] Feature Interaction Detection
- Jan. 2001: [CADP case study] Verification and Testing of Asynchronous Circuits
- Jan. 2001: [CADP case study] Conference Protocol
- Jan. 2001: [CADP-based tool] Timed Automata for Programmable Logic Controllers
- Jan. 2001: [CADP-based tool] ConcurTaskTrees Environment
- Jan. 2001: [CADP-based tool] Interaction Abstraction Algorithm
- Jan. 2001: [CADP-based tool] UMLAUT environment for UML
- Jan. 2001: [CADP-based tool] Labelled transition systems of B specifications
- Feb. 2001: VASY is seeking a software engineer (FormalFame project)
- Mar. 2001: Parallel State Space Construction for Model-Checking
- Apr. 2001: Reference Manual of OCIS (Open/Caesar Interactive Simulator)
- Apr. 2001: Reference Manual of SVL (Script Verification Language)
- Jun. 2001: VASY is seeking a software engineer (Parfums project)
- Jul. 2001: Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications
- Jul. 2001: SVL: a Scripting Language for Compositional Verification
- Aug. 2001: VASY is seeking a software engineer (FormalFame project)
- Sep. 2001: Scientific events recommended by the VASY team
- Oct. 2001: Scientific goals of the VASY team (updated)
- Oct. 2001: Frédéric Tronel's Home Page
- Oct. 2001: Dr. Gordon Pace's Home Page
- Nov. 2001: Miscellaneous CADP Resources
- Nov. 2001: Known problems and patches for CADP 2001 "Ottawa"
- Nov. 2001: Open PhD position at INRIA/VASY
- Dec. 2001: CADP Online Request Form
- Dec. 2001: Séminaire VASY 2001
2000
January 1st, 2000: VASY Becomes an Official INRIA Research Project
February 29, 2000: TRAIAN 2.0 is available for free download
November 14, 2000: TRAIAN 2.1 is available for free download
Other Additions to the VASY Web Site:
- Jan. 2000: Known Problems and Patches for CADP 97b "Liège"
- Jan. 2000: Rapport d'activité VASY 1999 (French)
- Feb. 2000: Etude de la migration et de la portabilité des applications informatiques d'Unix vers Windows NT
- Feb. 2000: Efficient Diagnostic Generation for Boolean Equation Systems
- Feb. 2000: Dr. Moez Cherif's Home Page
- Feb. 2000: Dr. Irina Smarandache's Home Page
- Feb. 2000: Case-studies achieved using the CADP toolset
- Feb. 2000: Research tools developed using the CADP toolset
- Mar. 2000: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
- May 2000: VASY is seeking a software engineer (FormalCard project)
- Jun. 2000: Nicolas Zuanon's Doctorate Defense (French)
- Jul. 2000: Dr. Nicolas Zuanon's Home Page
- Jul. 2000: Dr. Frédéric Lang's Home Page
- Aug. 2000: VASY is seeking a software engineer (Oural project)
- Sep. 2000: VASY is seeking a software engineer (FormalFame project)
- Nov. 2000: TRAIAN 2.1 is available for free download
- Nov. 2000: System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification...
- Nov. 2000: The Dyade/FormalCard Action
- Nov. 2000: The VASY Team within Dyade
- Nov. 2000: Rapport d'activité Dyade/FormalCard 2000
- Dec. 2000: Rapport d'activité Dyade/FormalFame 2000
1999
(Positive) Evaluation of the VASY-RA action (1997-1998) (Restricted access)
Dr Mihaela Sighireanu obtains a permanent position at University Paris 7
The work of VASY is cited in the Annual Report of INRIA 1999 (French or English)
"Validating Hardware Communication Architectures" [PDF or PostScript]
"La validation d'architectures matérielles de communication" [PDF or PostScript]
Other Additions to the VASY Web Site (Starting Late 1999):
- Sep. 1999: ERCIM Working Group on Formal Methods for Industrial Critical Systems
- Oct. 1999: CADP On-Line Manual Pages
- Nov. 1999: What do they think of VASY?
- Dec. 1999: REUTEL 2000 : Outils et techniques pour applications de télécommunications réutilisables
- Dec. 1999: The Dyade/Vasy and Dyade/FormalFame Actions
- Dec. 1999: Rapport d'activité Dyade/FormalFame 1999
1998
The University of Ottawa ranks 2nd at the Feature Interaction Contest
The work of VASY is cited in the Annual Report of INRIA 1998
"Logiciels : objectif zéro faute" (French) [PDF or PostScript]
or Software: objective zero default (English)Rapport d'activité VASY 1998 (French) [PDF or PostScript]
1997
1996
Version 1.510 - Date 12/03/12 19:54:27
Back to the VASY Home Page