@inproceedings{bbk-esop-92,
address = {Rennes, France},
month = feb,
year = 1992,
volume = 582,
series = {Lecture Notes in Computer Science},
nmpublisher = {Springer-Verlag},
publisher = {Springer},
editor = {Krieg-Br{\"u}ckner, Bernd},
acronym = {{ESOP}'92},
booktitle = {{P}roceedings of the 4th
{E}uropean {S}ymposium on {P}rogramming
({ESOP}'92)},
author = {Bernot, Gilles and Bidoit, Michel and
Knapik, Teodor},
title = {Towards an Adequate Notion of Observation},
pages = {39-55}
}
@inproceedings{mb-gb-amast-91,
address = {Iowa City, Iowa, USA},
year = 1992,
series = {Workshops in Computing},
publisher = {Springer-Verlag},
editor = {Nivat, Maurice and Rattray, Charles and Rus, Teodor
and Scollo, Giuseppe},
acronym = {{AMAST}'91},
booktitle = {{P}roceedings of the 2nd {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'91)},
author = {Bernot, Gilles and Bidoit, Michel},
title = {Proving the Correctness of Algebraically Specified
Software: {M}odularity and Observability Issues},
pages = {216-242},
note = {Invited paper}
}
@inproceedings{mb-ima-90,
address = {Stirling, Scotland, UK},
year = 1992,
publisher = {Oxford University Press},
editor = {Rattray, Charles and Clark, Robert G.},
booktitle = {{P}roceedings of the {IMA} {C}onference on the
{U}nified {C}omputation {L}aboratory},
author = {Bidoit, Michel},
title = {Development of Modular Specifications by Stepwise
Refinements Using the {PLUSS} Specification
Language},
pages = {171-192},
note = {Invited paper}
}
@inproceedings{bid-hen-obs-lp-92,
address = {Dedham, Massachusetts, USA},
year = 1993,
series = {Workshops in Computing},
publisher = {Springer-Verlag},
editor = {Martin, Ursula and Wing, Jeannette M.},
booktitle = {{P}roceedings of the 1st {I}nternational
{W}orkshop on {L}arch},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {How to Prove Observational Theorems with {LP}},
pages = {18-35}
}
@inproceedings{bid-hen-tapsoft,
address = {Orsay, France},
month = apr,
year = 1993,
volume = 668,
series = {Lecture Notes in Computer Science},
nmpublisher = {Springer-Verlag},
publisher = {Springer},
editor = {Gaudel, Marie-Claude and Jouannaud, Jean-Pierre},
acronym = {{TAPSOFT}'93},
booktitle = {{P}roceedings of the 5th
{I}nternational {J}oint {C}onference {CAAP}/{FASE} on
{T}heory and {P}ractice of {S}oftware {D}evelopment
({TAPSOFT}'93)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {A General Framework for Modular Implementations of
Modular Systems},
pages = {199-214}
}
@inproceedings{mb-cc-assp-lp-92,
address = {Dedham, Massachusetts, USA},
year = 1993,
series = {Workshops in Computing},
publisher = {Springer-Verlag},
editor = {Martin, Ursula and Wing, Jeannette M.},
booktitle = {{P}roceedings of the 1st {I}nternational
{W}orkshop on {L}arch},
author = {Choppy, {\relax Ch}ristine and Bidoit, Michel},
title = {Integrating {ASSPEGIQUE} and {LP}},
pages = {69-85}
}
@inproceedings{bid-hen-4th-alp,
address = {Madrid, Spain},
month = sep,
year = 1994,
volume = 850,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Levi, Giorgio and Rodriguez-Artalejo, Mario},
acronym = {{ALP}'94},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {A}lgebraic and {L}ogic {P}rogramming
({ALP}'94)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Proving Behavioural Theorems with Standard
First-Order Logic},
pages = {41-58}
}
@inproceedings{bid-hen-wir-5th-esop,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 1994,
volume = 788,
series = {Lecture Notes in Computer Science},
nmpublisher = {Springer-Verlag},
publisher = {Springer},
editor = {Sannella, Donald},
acronym = {{ESOP}'94},
booktitle = {{P}roceedings of the 5th
{E}uropean {S}ymposium on {P}rogramming
({ESOP}'94)},
author = {Bidoit, Michel and Hennicker, Rolf and
Wirsing, Martin},
title = {Characterizing Behavioural Semantics and Abstractor
Semantics},
pages = {105-119}
}
@article{gb-mb-tk-acta-obs,
publisher = {Springer},
journal = {Acta Informatica},
author = {Bernot, Gilles and Bidoit, Michel and
Knapik, Teodor},
title = {Behavioural Approaches to Algebraic Specifications:
{A} Comparative Study},
volume = {31},
number = {7},
pages = {651-671},
year = {1994},
month = oct
}
@inproceedings{bid-hen-10th-wadt,
address = {Santa Margherita, Italy},
year = 1995,
volume = 906,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Astesiano, Egidio and Reggio, Gianna and
Tarlecki, Andrzej},
acronym = {{ADT}'94},
booktitle = {{R}ecent {T}rends in {D}ata {T}ype {S}pecification~---
{S}elected {P}apers of the 10th {W}orkshop
on {S}pecification of {A}bstract {D}ata {T}ypes
({ADT}'94), joint with the 5th COMPASS Workshop},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Behavioural Theories},
pages = {153-169},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bid-hen-10th-wadt.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bid-hen-10th-wadt.ps}
}
@inproceedings{bid-hen-4th-amast,
address = {Montreal, Canada},
month = jul,
year = 1995,
volume = 936,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alagar, Vangalur S. and Nivat, Maurice},
acronym = {{AMAST}'95},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'95)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Proving the Correctness of Behavioural
Implementations},
pages = {152-168}
}
@techreport{bid-tar-rec-alg,
author = {Bidoit, Michel and Tarlecki, Andrzej},
title = {Regular Algebras: {A} Framework for Observational
Specifications with Recursive Definitions},
type = {Report},
number = {LIENS-95-12},
year = {1995},
month = may,
institution = {{\'E}cole Normale Sup{\'e}rieure, Paris, France}
}
@article{gb-mb-tk-tcs-obs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bernot, Gilles and Bidoit, Michel and
Knapik, Teodor},
title = {Observational Specifications and the
Indistinguishability Assumption},
volume = {139},
number = {1-2},
pages = {275-314},
year = {1995},
month = mar
}
@article{mb-rh-mw-scp-esop,
publisher = {Elsevier Science Publishers},
journal = {Science of Computer Programming},
author = {Bidoit, Michel and Hennicker, Rolf and
Wirsing, Martin},
title = {Behavioural and Abstractor Specifications},
volume = {25},
number = {2-3},
pages = {149-186},
year = {1995},
month = dec
}
@article{bid-hen-tcs-alp,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Behavioural Theories and the Proof of Behavioural
Properties},
volume = {165},
number = {1},
pages = {3-55},
year = {1996},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-RH-TCS-ALP.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-RH-TCS-ALP.ps}
}
@inproceedings{bid-tar-caap96,
address = {Link{\"o}ping, Sweden},
month = apr,
year = 1996,
volume = 1059,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kirchner, H{\'e}l{\`e}ne},
acronym = {{CAAP}'96},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}olloquium on {T}rees in {A}lgebra and
{P}rogramming
({CAAP}'96)},
author = {Bidoit, Michel and Tarlecki, Andrzej},
title = {Behavioural Satisfaction and Equivalence in Concrete
Model Categories},
pages = {241-256},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-AT-caap96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-AT-caap96.ps}
}
@inproceedings{fv-mb-wadt11,
address = {Oslo, Norway},
year = 1996,
volume = 1130,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haveraaen, Magne and Owe, Olaf and Dahl, Ole-Johan},
acronym = {{ADT}'95},
booktitle = {{R}ecent {T}rends in {D}ata {T}ype {S}pecification~---
{S}elected {P}apers of the 11th {W}orkshop
on {S}pecification of {A}bstract {D}ata {T}ypes
({ADT}'95), joint with the 8th COMPASS Workshop},
author = {Voisin, Fr{\'e}d{\'e}ric and Bidoit, Michel},
title = {Modular Algebraic Specifications and the Orientation
of Equations into Rewrite Rules},
pages = {503-521},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FV-MB-wadt96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FV-MB-wadt96.ps}
}
@inproceedings{mb-cc-fv-wadt11,
address = {Oslo, Norway},
year = 1996,
volume = 1130,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haveraaen, Magne and Owe, Olaf and Dahl, Ole-Johan},
acronym = {{ADT}'95},
booktitle = {{R}ecent {T}rends in {D}ata {T}ype {S}pecification~---
{S}elected {P}apers of the 11th {W}orkshop
on {S}pecification of {A}bstract {D}ata {T}ypes
({ADT}'95), joint with the 8th COMPASS Workshop},
author = {Bidoit, Michel and Choppy, {\relax Ch}ristine and
Voisin, Fr{\'e}d{\'e}ric},
title = {Interchange Format for Inter-Operability of Tools and
Translation, The {SALSA} and {ASSPEGIQUE\(^{\mathord{+}}\)/LP}
Experience},
pages = {102-124},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-CC-FV-wadt96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-CC-FV-wadt96.ps}
}
@incollection{steam-boiler,
month = oct,
year = 1996,
volume = 1165,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abrial, Jean-Raymond and B{\"o}rger, Egon and
Langmaack, Hans},
booktitle = {{F}ormal {M}ethods for {I}ndustrial {A}pplications:
{S}pecifying and {P}rogramming the {S}team {B}oiler {C}ontrol},
author = {Bidoit, Michel and Chevenier, Claude and
Pellen, {\relax Ch}ristine and Ryckbosch, J{\'e}r{\^o}me},
title = {An Algebraic Specification of the Steam-Boiler
Control System},
pages = {79-108},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCPR-lncs1165.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCPR-lncs1165.ps}
}
@techreport{forma-sric-BerBid-97,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel},
title = {Contribution du {LSV} {\`a} l'op{\'e}ration~2 <<~{\'E}tude de
cas {SRIC}~>>},
year = {1997},
month = oct,
type = {Contract Report},
institution = {Action FORMA},
note = {29 pages}
}
@article{hen-wir-bid-tcs-wadt,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Hennicker, Rolf and Wirsing, Martin and Bidoit, Michel},
title = {Proof Systems for Structured Specifications with
Observability Operators},
volume = {173},
number = {2},
pages = {393-443},
year = {1997},
month = feb
}
@incollection{plandedefense,
author = {Bidoit, Michel and Pellen, {\relax Ch}ristine and
Ryckbosch, J{\'e}r{\^o}me},
title = {Plan de D{\'e}fense~--- {F}ormalisation du cahier des
charges du {P}oint {C}entral {\`a} l'aide de sp{\'e}cifications
alg{\'e}briques},
booktitle = {Application des techniques formelles au logiciel},
chapter = {7},
type = {chapter},
pages = {123-132},
series = {ARAGO 20},
publisher = {Observatoire Fran\c{c}ais des Techniques Avanc\'ees},
year = {1997},
month = jun,
lsv-lang = {FR}
}
@techreport{BB-MB-AP-src98,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and
Petit, Antoine},
title = {Recommandations sur le cahier des charges {SRC}},
year = {1998},
missingmonth = {},
missingnmonth = {},
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@article{bid-hen-acta-amast,
publisher = {Springer},
journal = {Acta Informatica},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Modular Correctness Proofs of Behavioural
Implementations},
volume = {35},
number = {11},
pages = {951-1005},
year = {1998},
month = nov,
doi = {10.1007/s002360050149}
}
@book{docdor99,
author = {Schnoebelen, {\relax Ph}ilippe and
B{\'e}rard, B{\'e}atrice and Bidoit, Michel
and Laroussinie, Fran{\c{c}}ois and Petit, Antoine},
title = {V{\'e}rification de logiciels : techniques et
outils du model-checking},
year = {1999},
month = apr,
publisher = {Vuibert},
isbn = {2-7117-8646-3},
url = {http://www.vuibert.com/livre593.html},
lsv-lang = {FR}
}
@inproceedings{mb-don-at-amast98,
address = {Amazonia, Brasil},
month = jan,
year = 1999,
volume = 1548,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haeberer, Armando Martin},
acronym = {{AMAST}'98},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'98)},
author = {Bidoit, Michel and Sannella, Donald and Tarlecki, Andrzej},
title = {Architectural Specifications in {CASL}},
pages = {341-357},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ECS-LFCS-99-407.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ECS-LFCS-99-407.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ECS-LFCS-99-407.ps}
}
@inproceedings{mb-rh-amast98,
address = {Amazonia, Brasil},
month = jan,
year = 1999,
volume = 1548,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haeberer, Armando Martin},
acronym = {{AMAST}'98},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'98)},
author = {Hennicker, Rolf and Bidoit, Michel},
title = {Observational Logic},
pages = {263-277},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-RH-amast99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-RH-amast99.ps}
}
@inproceedings{mb-rolf-fm99,
address = {Toulouse, France},
month = sep,
year = 1999,
optaddress = {Bucharest, Romania},
publisher = {Theta, Bucharest, Romania},
editor = {Futatsugi, Kokichi and Goguen, Joseph and Meseguer, Jos{\'e}},
acronym = {{FM}'99},
booktitle = {{P}roceedings of the {OBJ}/{C}afe{OBJ}/{M}aude
{W}orkshop at {F}ormal {M}ethods
({FM}'99)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Observer Complete Definitions are Behaviourally
Coherent},
pages = {83-94},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CafeOBJ.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CafeOBJ.ps}
}
@incollection{proofsystems,
author = {Bidoit, Michel and Cengarle, Mar{\'\i}a Victoria and
Hennicker, Rolf},
title = {Proof systems for structured specifications and their
refinements},
editor = {Astesiano, Egidio and Kreowski, Hans-J{\"o}rg and
Krieg-Br{\"u}ckner, Bernd},
booktitle = {Algebraic Foundations of Systems Specification},
type = {chapter},
chapter = {11},
pages = {385-433},
year = {1999},
missingmonth = {},
missingnmonth = {},
publisher = {Springer},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ch11AFSSbook.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ch11AFSSbook.ps}
}
@inproceedings{tbhw-uml99,
address = {Fort Collins, Colorado, USA},
month = oct,
year = 1999,
volume = 1723,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {France, Robert B. and Rumpe, Bernhard},
acronym = {{UML}'99},
booktitle = {{P}roceedings of the 2nd {I}nternational
{C}onference on the {U}nified {M}odeling
{L}anguage
({UML}'99)},
author = {Bidoit, Michel and Hennicker, Rolf and
Tort, Fran{\c{c}}oise and Wirsing, Martin},
title = {Correct Realization of Interface Constraints with
{OCL}},
pages = {399-415},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TBHW-uml99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TBHW-uml99.ps}
}
@inproceedings{BB-wadt2001,
address = {Genova, Italy},
month = apr,
year = 2001,
volume = 2267,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cerioli, Maura and Reggio, Gianna},
acronym = {{WADT}'01},
booktitle = {{R}ecent {T}rends in {A}lgebraic {D}evelopment {T}echniques~---
{S}elected {P}apers of the 15th {I}nternational {W}orkshop
on {A}lgebraic {D}evelopment {T}echniques
({WADT}'01)},
author = {Bidoit, Michel and Boisseau, Alexandre},
title = {Algebraic Abstractions},
pages = {21-47},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-wadt2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-wadt2001.ps}
}
@misc{CASL-tut-2001,
author = {Bidoit, Michel and Mosses, Peter D.},
title = {A Gentle Introduction to {CASL}~v1.0.1},
year = {2001},
month = apr,
howpublished = {Invited tutorial, CoFI Workshop at the 4th European Joint Conferences on
Theory and Practice of Software (ETAPS 2001), Genova,
Italy},
url = {http://www.lsv.ens-cachan.fr/~bidoit/CASL/}
}
@inproceedings{bhk-fossacs2001,
address = {Genova, Italy},
month = apr,
year = 2001,
volume = 2030,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Honsell, Furio and Miculan, Marino},
acronym = {{FoSSaCS}'01},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'01)},
author = {Bidoit, Michel and Hennicker, Rolf and Kurz, Alexander},
title = {On the Duality between Observability and
Reachability},
pages = {72-87},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-fossacs2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-fossacs2001.ps}
}
@book{lsvmcbook01,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Finkel, Alain
and Laroussinie, Fran{\c{c}}ois and
Petit, Antoine and Petrucci, Laure and
Schnoebelen, {\relax Ph}ilippe},
title = {Systems and Software Verification. {M}odel-Checking
Techniques and Tools},
year = {2001},
missingmonth = {},
missingnmonth = {},
publisher = {Springer},
isbn = {3-540-41523-8},
url = {http://www.springer.com/978-3-540-41523-8},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41523-8}
}
@article{BST-FAC2002,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bidoit, Michel and Sannella, Donald and
Tarlecki, Andrzej},
title = {Architectural Specifications in {CASL}},
volume = {13},
number = {3-5},
pages = {252-273},
year = {2002},
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-FAC2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-FAC2002.ps},
doi = {10.1007/s001650200012}
}
@inproceedings{BST-mfcs2002,
address = {Warsaw, Poland},
month = aug,
year = 2002,
volume = 2420,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Diks, Krzysztof and Rytter, Wojciech},
acronym = {{MFCS}'02},
booktitle = {{P}roceedings of the 27th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'02)},
author = {Bidoit, Michel and Sannella, Donald and
Tarlecki, Andrzej},
title = {Global Development via Local Observational
Construction Steps},
pages = {1-24},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-MFCS02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-MFCS02.ps}
}
@incollection{HHB-OCL,
missingnmonth = {},
missingmonth = {},
year = 2002,
volume = 2263,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Clark, Tony and Warmer, Jos},
booktitle = {{O}bject {M}odeling with the {OCL}~---
{T}he {R}ationale behind the {O}bject {C}onstraint {L}anguage},
author = {Hennicker, Rolf and Hu{\ss}mann, Heinrich and
Bidoit, Michel},
title = {On the Precise Meaning of {OCL} Constraints},
pages = {69-84},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HBB-oclBook.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HBB-oclBook.ps}
}
@inproceedings{bh-fossacs2002,
address = {Grenoble, France},
month = apr,
year = 2002,
volume = 2303,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Engberg, Uffe},
acronym = {{FoSSaCS}'02},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'02)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {On the Integration of Observability and Reachability
Concepts},
pages = {21-36},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BidHenFossacs02SHORT.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
BidHenFossacs02SHORT.ps}
}
@article{bid-etalias-casl-tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Astesiano, Egidio and Bidoit, Michel and
Kirchner, H{\'e}l{\`e}ne
and Krieg-Br{\"u}ckner, Bernd and Mosses, Peter D. and
Sannella, Donald and Tarlecki, Andrzej},
title = {{CASL}: {T}he {C}ommon {A}lgebraic {S}pecification
{L}anguage},
volume = {286},
number = {2},
pages = {153-196},
year = {2002},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CASL-TCS01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CASL-TCS01.ps}
}
@article{bhk-tcs-fossacs01,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bidoit, Michel and Hennicker, Rolf and
Kurz, Alexander},
title = {Observational Logic, Constructor-Based Logic, and
their Duality},
volume = {298},
number = {3},
pages = {471-510},
year = {2003},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-TCS-FOSSACS01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-TCS-FOSSACS01.ps}
}
@book{CASL-LNCS,
author = {Bidoit, Michel and Mosses, Peter D.},
title = {{CASL} User Manual~--- Introduction to Using the
Common
Algebraic Specification Language},
volume = {2900},
series = {Lecture Notes in Computer Science},
year = {2004},
publisher = {Springer},
isbn10 = {3-540-20766-X},
isbn = {978-3-540-20766-5},
doi = {10.1007/b11968},
url = {http://www.springer.com/978-3-540-20766-X},
oldurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-20766-X}
}
@inproceedings{bh-amast2004,
address = {Stirling, UK},
month = jul,
year = 2004,
volume = 3116,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rattray, Charles and Maharaj, Savitri and Shankland, Carron},
acronym = {{AMAST}'04},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'04)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Glass Box and Black Box Views of State-Based System
Specifications},
pages = {19},
note = {Invited talk}
}
@inproceedings{bhkb-sefm2004,
address = {Beijing, China},
month = sep,
year = 2004,
publisher = {{IEEE} Computer Society Press},
acronym = {{SEFM}'04},
booktitle = {{P}roceedings of the 2nd {IEEE} {I}nternational
{C}onference on {S}oftware {E}ngineering and
{F}ormal {M}ethods
({SEFM}'04)},
author = {Bidoit, Michel and Hennicker, Rolf and
Knapp, Alexander
and Baumeister, Hubert},
title = {Glass-Box and Black-Box Views on Object-Oriented
Specifications},
pages = {208-217},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhkb-sefm2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhkb-sefm2004.pdf},
doi = {10.1109/SEFM.2004.10014}
}
@inproceedings{bst-monterey,
address = {Venice, Italy},
year = 2004,
volume = 2941,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wirsing, Martin and Knapp, Alexander and
Balsamo, Simonetta},
acronym = {{RISSEF}'02},
booktitle = {{R}evised {P}apers of the 9th {I}nternational
{W}orkshop on {R}adical {I}nnovations of {S}oftware
and {S}ystems {E}ngineering in the {F}uture
({RISSEF}'02)},
author = {Bidoit, Michel and Sannella, Donald and
Tarlecki, Andrzej},
title = {Toward Component-Oriented Formal Software
Development:
{A}n Algebraic Approach},
pages = {75-90},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BST-monterey.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BST-monterey.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BST-monterey.pdf}
}
@inproceedings{BH-ICTAC05,
address = {Hanoi, Vietnam},
month = oct,
year = 2005,
volume = 3722,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hung, Dang Van and Wirsing, Martin},
acronym = {{ICTAC}'05},
booktitle = {{P}roceedings of the 2nd {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'05)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Externalized and Internalized Notions of Behavioral
Refinement},
pages = {334-350},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf},
doi = {10.1007/11560647_22},
abstract = {Many different behavioral refinement notions for algebraic
specifications have been proposed in the literature but the relationship
between the various concepts is still unclear. In this paper we provide a
classification and a comparative study of behavioral refinements according
to two directions, the externalized approach which uses an explicit
behavioral abstraction operator that is applied to the specification to
be implemented, and the internalized approach which uses a built-in
behavioral semantics of specifications. We show that both concepts are
equivalent under suitable conditions. The formal basis of our study is
provided by the COL institution (constructor-based observational logic).
Hence, as a side-effect of our study on internalized behavioral refinements,
we introduce also a novel concept of behavioral refinement for
COL-specifications.}
}
@article{bid-hen-JLAP-2005,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Programming},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Constructor-Based Observational Logic},
year = {2006},
month = apr # {-} # may,
number = {1-2},
volume = 67,
pages = {3-51},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf},
doi = {10.1016/j.jlap.2005.09.002},
abstract = {This paper focuses on the integration of reachability and
observability concepts within an algebraic,
institution-based framework. In the first part of this work,
we develop the essential ingredients that are needed to define the
constructor-based observational logic institution, called
COL, which takes into account both
the generation- and observation-oriented aspects of software systems. The
underlying paradigm of our approach is that the semantics of a specification should be as
loose as possible to capture all its correct realizations. We also consider the {"}black
box{"} semantics of a specification which is useful to study the behavioral properties
a user can observe when he\slash she is experimenting with the system.\par
In the second part of this work, we develop proof techniques for structured
COL-specifications. For this purpose we introduce an
institution encoding from the COL
institution to the institution of many-sorted first-order logic with equality
and sort-generation constraints. Using this institution
encoding, we can then reduce proofs of
consequences of structured specifications built over COL to proofs of consequences
of structured specifications written in a simple subset of the algebraic specification
language {\scshape Casl}. This means, in particular, that any inductive theorem prover, such
as \emph{e.g.} the Larch Prover or PVS, can be used to prove theorems over structured
COL-specifications.}
}
@inproceedings{BH-Goguen06,
address = {San Diego, California, USA},
month = jun,
year = 2006,
volume = 4060,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Futatsugi, Kokichi and Jouannaud, Jean-Pierre and
Meseguer, Jos{\'e}},
acronym = {{A}lgebra, {M}eaning and {C}omputation},
booktitle = {{A}lgebra, {M}eaning and {C}omputation~--- Essays dedicated to
Joseph~A.~Goguen on the Occasion of His 65th~Birthday},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Proving Behavioral Refinements of {COL}-Specifications},
pages = {333-354},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf},
doi = {10.1007/11780274_18},
abstract = {The COL institution (constructor-based
observational logic) has been introduced as a formal
framework to specify both generation- and
observation-oriented properties of software systems. In
this paper we consider behavioral refinement relations
between COL-specifications taking into account
implementation constructions. We propose a general
strategy for proving the correctness of such
refinements by reduction to (standard) first-order
theorem proving with induction. Technically our
strategy relies on appropriate proof rules and on a
lifting construction to encode the reachability and
observability notions of the COL institution.}
}
@article{BST-mscs08,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Bidoit, Michel and Sannella, Donald and Tarlecki, Andrzej},
title = {Observational Interpretation of {\textsc{\MakeUppercase{C}asl}}
Specifications},
volume = 18,
number = 2,
pages = {325-371},
month = apr,
year = 2008,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-16.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-16.pdf},
doi = {10.1017/S0960129507006536},
noaxelsv = {???},
abstract = {The way that refinement of individual {"}local{"} components of a
specification relates to development of a {"}global{"} system from a
specification of requirements is explored. Observational interpretation of
specifications and refinements add expressive power and flexibility while
bringing in some subtle problems. Our~study of these issues is carried out in
the context of~\textsc{Casl} architectural specifications. We~introduce a
definition of observational equivalence for \textsc{Casl} models, leading to
an observational semantics for architectural specifications for which we prove
important properties. Overall, this fulfills the long-standing goal of
complementing the standard semantics of \textsc{Casl} specifications with an
observational view that supports observational refinement of specifications in
combination with \textsc{Casl}-style architectural design.}
}
@inproceedings{BH-amast08,
address = {Urbana, Illinois, USA},
month = jul,
year = 2008,
volume = 5140,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Meseguer, Jos{\'e} and Rosu, Grigore},
acronym = {{AMAST}'08},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'08)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {An Algebraic Semantics for Contract-Based Software Components},
pages = {216-231},
doi = {10.1007/978-3-540-79980-1_17},
noaxelsv = {???},
abstract = {We propose a semantic foundation for the contract-based design
of software components. Our approach focuses on the
characteristic principles of component-oriented development,
like provided and required interface specifications and
strong encapsulation. Semantically, we adopt classical
concepts of mathematical logic using models, in our
framework given by labelled transition systems with {"}states
as algebras{"}, sentences, and a satisfaction relation which
characterizes those properties of a component which are
observable by the user in the {"}strongly reachable{"} states.
We distinguish between models of interfaces and models of
component bodies. The latter are equipped with semantic
encapsulation constraints which guarantee, that if the
component body is a correct user of the required interface
operations, then it can safely rely on all properties of the
required interface specification. Our model-theoretic
semantics of interfaces and component bodies suggests two
semantic views on a component, its external and its internal
semantics which must be properly related to ensure the
correctness of a component. We also study a refinement
relation between required and provided interface
specifications of different components used for component
composition.}
}
@inproceedings{BHB-sbmf10,
address = {},
month = nov,
year = 2010,
volume = 6527,
series = {Lecture Notes in Computer Science},
editor = {Davies, Jim and Silva, Leila and da~Silva Sim{\~a}o, Adenilso},
publisher = {Springer},
acronym = {{SBMF}'10},
booktitle = {{R}evised {S}elected {P}apers of the 13th {B}razilian {S}ymposium on {F}ormal
{M}ethods ({SBMF}'10)},
author = {Bauer, Sebastian S. and Hennicker, Rolf and Bidoit, Michel},
title = {A~Modal Interface Theory with Data Constraints},
pages = {80-95},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHB-sbmf10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHB-sbmf10.pdf},
doi = {10.1007/978-3-642-19829-8_6},
abstract = {For the design of component-based software, the behavioral
specification of component interfaces is crucial. We propose an extension
of the theory of modal I{\slash}O-transition systems by Larsen
\textit{et~al.} to cope with both control flow and data states of reactive
components at the same time. In our framework, transitions model incoming
or outgoing operation calls which are constrained by pre- and
postconditions expressing the mutual assumptions and guarantees of the
receiver and the sender of a message. We define a new interface theory by
adapting synchronous composition, modal refinement and modal compatibility
to the case of modal I{\slash}O-transition systems with data constraints.
We show that in this formalism modal compatibility is preserved by
refinement and modal refinement is preserved by composition which are
basic requirements for any interface theory.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
This file was generated by bibtex2html 1.98.