|
What's New on the VASY Web Server? |
The VASY team completed its activities on December 2011. Past this date, this Web site will no longer be updated regularly, except by adding contents that were elaborated during the existence of VASY or that are directly relevant to VASY.
See also the two following sites, which are actively maintained:
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
- Oct. 2011: Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols (slides of R. Mateescu's lecture at SAFA'11)
- Oct. 2011: Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP (slides of W. Serwe's lecture at FMICS'11)
- Nov. 2011: Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP (slides of G. Salaün's lecture at FM'11)
- Nov. 2011: Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP
- Dec. 2011: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes (slides of H. Garavel's lecture at TACAS'11)
- Dec. 2011: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes (slides of H. Garavel's lecture at the LASER 2011 summer school)
- Dec. 2011: Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
- Dec. 2011: Self-configuration of Legacy Distributed Applications in the Cloud
- Jul. 2012: Damien Thivolle's Doctorate Thesis (PDF)
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.534 - Date 2024/02/05 11:53:52
Back to the VASY Home Page