@article(S1S-tcad2000,
 author       = {A. Aziz and F. Balarin and R.K. Brayton and Sangiovanni-Vincentelli, A. L.},
 year         = {2000},
 title        = {{Sequential synthesis using S1S}},
 journal      = {IEEE Transactions on Computer-Aided Design},
 volume       = {19},
 number       = {10},
 pages        = {1149--1162},
 doi          = {10.1109/43.875301},
)
@article(barrett-deds98,
 author       = {G. Barrett and S. Lafortune},
 year         = {1998},
 title        = {Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines},
 journal      = {Discrete Event Dynamic Systems: Theory \& Applications},
 volume       = {8},
 number       = {4},
 pages        = {377--429},
 doi          = {10.1023/A:1008301317459},
)
@inproceedings(benes2013,
 author       = {Bene{\v{s}}, Nikola and Beno{\^i}t Delahaye and Uli Fahrenberg and K{\v{r}}et{\'i}nsk{\'y}, Jan and Axel Legay},
 year         = {2013},
 title        = {Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory},
 editor       = {Pedro R. D'Argenio and Hern{\'a}n Melgratti},
 booktitle    = {CONCUR 2013 -- Concurrency Theory},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {76--90},
 doi          = {10.1007/978-3-642-40184-8_7},
)
@inproceedings(multViewpoint,
 author       = {A. Benveniste and B. Caillaud and A. Ferrari and L. Mangeruca and R. Passerone and C. Sofronis},
 year         = {2007},
 title        = {Multiple Viewpoint Contract-Based Specification and Design},
 editor       = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem-Paul de Roever},
 booktitle    = {Formal Methods for Components and Objects},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {200--225},
 doi          = {10.1007/978-3-540-92188-2_9},
)
@article(BenvenisteContractBook,
 author       = {A. Benveniste and B. Caillaud and D. Nickovic and R. Passerone and J.-B. Raclet and P. Reinkemeier and Sangiovanni-Vincentelli, A. L. and W. Damm and T. A. Henzinger and K. G. Larsen},
 year         = {2018},
 title        = {Contracts for System Design},
 journal      = {Foundations and Trends$^{\text{\relax\fontsize {8}{9.5}\selectfont{\textregistered}}}$\hspace{-.3em} in Electronic Design Automation},
 volume       = {12},
 number       = {2-3},
 pages        = {124--400},
 doi          = {10.1561/1000000053},
)
@article(bhaduri08,
 author       = {P. Bhaduri and S. Ramesh},
 year         = {2008},
 title        = {Interface synthesis and protocol conversion},
 journal      = {Formal Asp. Comput.},
 volume       = {20},
 number       = {2},
 pages        = {205--224},
 doi          = {10.1007/s00165-007-0045-4},
)
@article(bochmann-deds2013,
 author       = {G. Bochmann},
 year         = {2013},
 title        = {Using logic to solve the submodule construction problem},
 journal      = {Discrete Event Dynamic Systems},
 volume       = {23},
 number       = {1},
 pages        = {27--59},
 doi          = {10.1007/s10626-011-0127-6},
)
@article(bouyer2011,
 author       = {Patricia Bouyer and Franck Cassez and Fran{\c{c}}ois Laroussinie},
 year         = {2011},
 title        = {Timed Modal Logics for Real-Time Systems - Specification, Verification and Control},
 journal      = {Journal of Logic, Language and Information},
 volume       = {20},
 number       = {2},
 pages        = {169--203},
 doi          = {10.1007/s10849-010-9127-4},
)
@inproceedings(burch-comb-cycle,
 author       = {J.R. Burch and D. Dill and E. Wolf and G. DeMicheli},
 year         = {1993},
 title        = {Modelling hierarchical combinational circuits},
 booktitle    = {The Proceedings of the International Conference on Computer-Aided Design},
 pages        = {612--617},
 doi          = {10.1109/ICCAD.1993.580149},
)
@inproceedings(cassez2000,
 author       = {Franck Cassez and Fran{\c{c}}ois Laroussinie},
 year         = {2000},
 title        = {Model-Checking for Hybrid Systems by Quotienting and Constraints Solving},
 editor       = {E. Allen Emerson and Aravinda Prasad Sistla},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {373--388},
 doi          = {10.1007/10722167_29},
)
@inproceedings(Castagnetti:SEFM-2015,
 author       = {G. Castagnetti and M. Piccolo and T. Villa and N. Yevtushenko and R. K. Brayton and A. Mishchenko},
 year         = {2015},
 title        = {Automated Synthesis of Protocol Converters with {BALM-II}},
 editor       = {D. Bianculli and R. Calinescu and B. Rumpe},
 booktitle    = {Software Engineering and Formal Methods. SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART. York, UK, September 7-8, 2015},
 pages        = {281--296},
 doi          = {10.1007/978-3-662-49224-6_23},
)
@article(cerny-marin77,
 author       = {E. Cerny and M. Marin},
 year         = {1977},
 title        = {An approach to unified methodology of combinational switching circuits},
 journal      = {IEEE Transactions on Computers},
 volume       = {vol. C-26},
 number       = {8},
 pages        = {745--756},
 doi          = {10.1109/TC.1977.1674912},
)
@incollection(verhoeff-mpc1989,
 author       = {W. Chen and J. Udding and T. Verhoeff},
 year         = {1989},
 title        = {Networks of communicating processes and their \unhbox\voidb@x \hbox{(de-)composition}},
 editor       = {J.L.A. van de Snepscheut},
 booktitle    = {Mathematics of Program Construction},
 series       = {Lecture Notes in Computer Science},
 volume       = {375},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {174--196},
 doi          = {10.1007/3-540-51305-1_10},
)
@inproceedings(dealfaro-interface03,
 author       = {De Alfaro, L.},
 year         = {2003},
 title        = {Game Models for Open Systems},
 editor       = {N. Dershowitz},
 booktitle    = {Verification: Theory and Practice},
 series       = {Lecture Notes in Computer Science},
 volume       = {2772},
 publisher    = {Springer Verlag},
 pages        = {269--289},
 doi          = {10.1007/978-3-540-39910-0_12},
)
@article(deAlfaro2001,
 author       = {De Alfaro, L. and T. A. Henzinger},
 year         = {2001},
 title        = {Interface Automata},
 journal      = {SIGSOFT Softw. Eng. Notes},
 volume       = {26},
 number       = {5},
 pages        = {109--120},
 doi          = {10.1145/503209.503226},
)
@article(mm-tac01,
 author       = {Di Benedetto, M. D. and Sangiovanni-Vincentelli, A. and T. Villa},
 year         = {2001},
 title        = {{Model Matching for Finite State Machines}},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {46},
 number       = {11},
 pages        = {1726--1743},
 doi          = {10.1109/9.964683},
)
@inproceedings(iwls10:ch2,
 author       = {M. Fujita and Y. Matsunaga and M. Ciesielski},
 year         = {2001},
 title        = {Multi-Level Logic Optimization},
 editor       = {R. Brayton and S. Hassoun and T. Sasao},
 booktitle    = {Logic Synthesis and Verification},
 publisher    = {Kluwer},
 pages        = {29--63},
 doi          = {10.1007/978-1-4615-0817-5_2},
)
@article(green-tcomm-1986,
 author       = {P. Green},
 year         = {1986},
 title        = {Protocol Conversion},
 journal      = {IEEE Transactions on Communications},
 volume       = {34},
 number       = {3},
 pages        = {257--268},
 doi          = {10.1109/32.4655},
)
@article(haghverdi99,
 author       = {E. Haghverdi and H. Ural},
 year         = {1999},
 title        = {Submodule construction from concurrent system specifications},
 journal      = {Information and Software Technology},
 volume       = {41},
 number       = {8},
 pages        = {499--506},
 doi          = {10.1016/S0950-5849(99)00014-2},
)
@inproceedings(hallal-conv2000,
 author       = {H. Hallal and R. Negulescu and A. Petrenko},
 year         = {2000},
 title        = {Design of divergence-free protocol converters using supervisory control techniques},
 booktitle    = {7th IEEE International Conference on Electronics, Circuits and Systems, ICECS 2000},
 volume       = {2},
 pages        = {705--708},
 doi          = {10.1109/ICECS.2000.912975},
)
@inproceedings(iwls10:ch9,
 author       = {S. Hassoun and T. Villa},
 year         = {2001},
 title        = {Optimization of Synchronous Circuits},
 editor       = {R. Brayton and S. Hassoun and T. Sasao},
 booktitle    = {Logic Synthesis and Verification},
 publisher    = {Kluwer},
 pages        = {225--253},
 doi          = {10.1007/978-1-4615-0817-5_2},
)
@book(ullman-automata2,
 author       = {J.E. Hopcroft and R. Motwani and J.D. Ullman},
 year         = {2001},
 title        = {{Introduction to Automata Theory, Languages, and Computation}},
 publisher    = {Addison-Wesley Publishing Company},
 doi          = {10.1145/568438.568455},
)
@book(fsm1-book,
 author       = {T. Kam and T. Villa and R. K. Brayton and Sangiovanni-Vincentelli, A. L.},
 year         = {1997},
 title        = {Synthesis of {FSM}s: Functional Optimization},
 publisher    = {Kluwer Academic Publishers},
 address      = {Boston},
 doi          = {10.1007/978-1-4757-2622-0},
)
@article(kim72,
 author       = {J. Kim and M.M. Newborn},
 year         = {1972},
 title        = {{The simplification of sequential machines with input restrictions}},
 journal      = {IRE Transactions on Electronic Computers},
 pages        = {1440--1443},
 doi          = {10.1109/T-C.1972.223521},
)
@article(kumar-conv97,
 author       = {R. Kumar and S. Nelvagal and S.I. Marcus},
 year         = {1997},
 title        = {A discrete event systems approach for protocol conversion},
 journal      = {Discrete Event Dynamic Systems: Theory \& Applications},
 volume       = {7},
 number       = {3},
 pages        = {295--315},
 doi          = {10.1023/A:1008258331497},
)
@article(kurshan-asynch99,
 author       = {R.P. Kurshan and M. Merritt and A. Orda and S.R. Sachs},
 year         = {1999},
 title        = {Modelling asynchrony with a synchronous model},
 journal      = {Formal Methods in System Design},
 volume       = {vol. 15},
 number       = {no. 3},
 pages        = {175--199},
 doi          = {10.1007/3-540-60045-0_61},
)
@article(lam-tse-1988,
 author       = {S. S. Lam},
 year         = {1988},
 title        = {Protocol Conversion},
 journal      = {IEEE Trans. Softw. Eng.},
 volume       = {14},
 number       = {3},
 pages        = {353--362},
 doi          = {10.1109/32.4655},
)
@inproceedings(larsen-xinxin1990,
 author       = {K.G. Larsen and L. Xinxin},
 year         = {1990},
 title        = {Equation solving using modal transition systems},
 booktitle    = {Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e},
 pages        = {108--117},
 doi          = {10.1109/LICS.1990.113738},
)
@article(lynch-cwi89,
 author       = {N. Lynch and M. Tuttle},
 year         = {1989},
 title        = {An introduction to Input/Output automata},
 journal      = {CWI-Quarterly},
 volume       = {2},
 number       = {3},
 pages        = {219--246},
 doi          = {10.1.1.83.7751},
)
@inproceedings(mallon99,
 author       = {W.C. Mallon and J.T. Tijmen and T. Verhoeff},
 year         = {1999},
 title        = {Analysis and Applications of the {XDI} Model},
 booktitle    = {International Symposium on Advanced Research in Asynchronous Circuits and Systems},
 pages        = {231--242},
 doi          = {10.1109/ASYNC.1999.761537},
)
@article(boch83,
 author       = {P. Merlin and G. v. Bochmann},
 year         = {1983},
 title        = {On the Construction of Submodule Specifications and Communication Protocols},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {5},
 number       = {1},
 pages        = {1--25},
 doi          = {10.1145/357195.357196},
)
@inproceedings(negu-concur00,
 author       = {R. Negulescu},
 year         = {2000},
 title        = {Process spaces},
 editor       = {C. Palamidessi},
 booktitle    = {Proceedings of CONCUR 2000, 11th International Conference on Concurrency Theory},
 series       = {LNCS},
 volume       = {1877},
 publisher    = {Springer-Verlag},
 pages        = {199--213},
 doi          = {10.1007/3-540-44618-4_16},
)
@inproceedings(DBLP:conf/iccad/PasseroneAHS02,
 author       = {R. Passerone and De Alfaro, L. and T. A. Henzinger and Sangiovanni-Vincentelli, A. L.},
 year         = {2002},
 title        = {Convertibility verification and converter synthesis: two faces of the same coin},
 editor       = {Lawrence T. Pileggi and Andreas Kuehlmann},
 booktitle    = {ICCAD},
 publisher    = {ACM},
 pages        = {132--139},
 url          = {http://doi.acm.org/10.1145/774572.774592},
)
@article(contractMerging,
 author       = {R. Passerone and {\'I}ncer Romeo, {\'I}. and Sangiovanni-Vincentelli, A. L.},
 year         = {2019},
 title        = {Coherent Extension, Composition, and Merging Operators in Contract Models for System Design},
 journal      = {ACM Trans. Embed. Comput. Syst.},
 volume       = {18},
 number       = {5s},
 doi          = {10.1145/3358216},
)
@inproceedings(DBLP:conf/dac/PasseroneRS98,
 author       = {R. Passerone and J. A. Rowson and Sangiovanni-Vincentelli, A. L.},
 year         = {1998},
 title        = {Automatic Synthesis of Interfaces Between Incompatible Protocols},
 booktitle    = {DAC},
 pages        = {8--13},
 url          = {http://doi.acm.org/10.1145/277044.277047},
)
@article(raclet2011modal,
 author       = {J.-B. Raclet and E. Badouel and A. Benveniste and B. Caillaud and A. Legay and R. Passerone},
 year         = {2011},
 title        = {A modal interface theory for component-based design},
 journal      = {Fundamenta Informaticae},
 volume       = {108},
 number       = {1-2},
 pages        = {119--149},
 doi          = {10.3233/FI-2011-416},
)
@inproceedings(agquotient,
 author       = {\'{I}ncer Romeo, \'{I}. and Sangiovanni-Vincentelli, A. L. and C.-W. Lin and E. Kang},
 year         = {2018},
 title        = {Quotient for Assume-Guarantee Contracts},
 booktitle    = {16th ACM-IEEE International Conference on Formal Methods and Models for System Design},
 series       = {MEMOCODE ’18},
 pages        = {67–77},
 doi          = {10.1109/MEMCOD.2018.8556872},
)
@inproceedings(iwls10:ch3,
 author       = {E. Sentovich and D. Brand},
 year         = {2001},
 title        = {Flexibility in Logic},
 editor       = {R. Brayton and S. Hassoun and T. Sasao},
 booktitle    = {Logic Synthesis and Verification},
 publisher    = {Kluwer},
 pages        = {65--88},
 doi          = {10.1007/978-1-4615-0817-5_2},
)
@article(ucp-ieeeproc2015,
 author       = {T. Villa and A. Petrenko and N. Yevtushenko and A. Mishchenko and R. K. Brayton},
 year         = {2015},
 title        = {Component-Based Design by Solving Language Equations},
 journal      = {Proceedings of the IEEE},
 volume       = {103},
 number       = {11},
 pages        = {2152--2167},
 doi          = {10.1109/JPROC.2015.2450937},
)
@book(villa12,
 author       = {T. Villa and N. Yevtushenko and R. K. Brayton and A. Mishchenko and A. Petrenko and Sangiovanni-Vincentelli, A. L.},
 year         = {2012},
 title        = {The Unknown Component Problem: Theory and Applications},
 publisher    = {Springer},
 doi          = {10.1007/978-0-387-68759-9},
)
@inproceedings(fujita-aspdac2007,
 author       = {S. Watanabe and K. Seto and Y. Ishikawa and S. Komatsu and M. Fujita},
 year         = {2007},
 title        = {Protocol Transducer Synthesis using Divide and Conquer approach},
 booktitle    = {Design Automation Conference, 2007. ASP-DAC '07. Asia and South Pacific},
 pages        = {280--285},
 doi          = {10.1109/ASPDAC.2007.357999},
)
@inproceedings(fsmeq1-iwls2004,
 author       = {N. Yevtushenko and T. Villa and R. K. Brayton and A. Mishchenko and Sangiovanni-Vincentelli, A. L.},
 year         = {2004},
 title        = {Composition Operators in Language Equations},
 booktitle    = {International Workshop on Logic and Synthesis},
 pages        = {409--415},
)