NOVA: State Assignment of Finite State Machines for Optimal Two-level Logic Implementations. - Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (DAC, 1989)

NOVA: state assignment of finite state machines for optimal two-level logic implementation. - Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1990)

A Framework for Satisfying Input and Output Encoding Constraints. - Alexander Saldanha; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (DAC, 1991)

Experiments on the synthesis and testability of non-scan finite state machines. - Michael Pabst; Tiziano Villa; A. Richard Newton (EURO-DAC, 1992)

A Fully Implicit Algorithm for Exact State Minimization. - Timothy Kam; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (DAC, 1994)

Satisfaction of input and output encoding constraints. - Alexander Saldanha; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Implicit state minimization of non-deterministic FSMs. - Timothy Kam; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (ICCD, 1995)

VIS: A System for Verification and Synthesis. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli; Fabio Somenzi; Adnan Aziz; Szu-Tsung Cheng; Stephen A. Edwards; Sunil P. Khatri; Yuji Kukimoto; Abelardo Pardo; Shaz Qadeer; Rajeev K. Ranjan 001; et al. (CAV, 1996)

VIS. - Robert K. Brayton; Gary D. Hachtel; Alberto L. Sangiovanni-Vincentelli; Fabio Somenzi; Adnan Aziz; Szu-Tsung Cheng; Stephen A. Edwards; Sunil P. Khatri; Yuji Kukimoto; Abelardo Pardo; Shaz Qadeer; Rajeev K. Ranjan 001; et al. (FMCAD, 1996)

Negative thinking by incremental problem solving: application to unate covering. - Evguenii I. Goldberg; Luca P. Carloni; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (ICCAD, 1997)

A fast and robust exact algorithm for face embedding. - Evguenii I. Goldberg; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (ICCAD, 1997)

Implicit computation of compatible sets for state minimization of ISFSMs. - Timothy Kam; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

Theory and algorithms for state minimization of nondeterministic FSMs. - Timothy Kam; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

Explicit and implicit algorithms for binate covering problems. - Tiziano Villa; Timothy Kam; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

Symbolic two-level minimization. - Tiziano Villa; Alexander Saldanha; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

An Exact Input Encoding Algorithm for BDDs Representing FSMs. - Wilsin Gosti; Alberto L. Sangiovanni-Vincentelli; Tiziano Villa; Alexander Saldanha (Great Lakes Symposium on VLSI, 1998)

Exact Minimization of Binary Decision Diagrams Using Implicit Techniques. - Arlindo L. Oliveira; Luca P. Carloni; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Computers, 1998)

Theory and algorithms for face hypercube embedding. - Evguenii I. Goldberg; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998)

Aura II: Combining Negative Thinking and Branch-and-Bound in Unate Covering Problems. - Luca P. Carloni; Evguenii I. Goldberg; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (VLSI, 1999)

Hybrid controller synthesis for idle speed management of an automotive engine. - Andrea Balluchi; Luca Benvenuti; Maria Domenica Di Benedetto; Tiziano Villa; Howard Wong-Toi; Alberto L. Sangiovanni-Vincentelli (ACC, 2000)

Maximal Safe Set Computation for Idle Speed Control of an Automotive Engine. - Andrea Balluchi; Luca Benvenuti; Maria Domenica Di Benedetto; Guido M. Miconi; Ugo Pozzi; Tiziano Villa; Howard Wong-Toi; Alberto L. Sangiovanni-Vincentelli (HSCC, 2000)

Negative thinking in branch-and-bound: the case of unate covering. - Evguenii I. Goldberg; Luca P. Carloni; Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000)

Solution of Parallel Language Equations for Logic Synthesis. - Nina Yevtushenko 001; Tiziano Villa; Robert K. Brayton; Alexandre Petrenko; Alberto L. Sangiovanni-Vincentelli (ICCAD, 2001)

Model matching for finite-state machines. - Maria Domenica Di Benedetto; Alberto L. Sangiovanni-Vincentelli; Tiziano Villa (IEEE Trans. Autom. Control., 2001)

Optimization of Multi-Valued Multi-Level Networks. - Robert K. Brayton; M. Gao; Jie-Hong Roland Jiang; Yunjian Jiang; Yinghua Li; Alan Mishchenko; Subarnarekha Sinha; Tiziano Villa (ISMVL, 2002)

Equisolvability of Series vs. Controller's Topology in Synchronous Language Equations. - Nina Yevtushenko 001; Tiziano Villa; Robert K. Brayton; Alexandre Petrenko; Alberto L. Sangiovanni-Vincentelli (IWLS, 2002)

Improving reachability analysis of hybrid automata for engine control. - Alberto Casagrande; Andrea Balluchi; Luca Benvenuti; Alberto Policriti; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (CDC, 2004)

FSM re-engineering and its application in low power state encoding. - Lin Yuan; Gang Qu 001; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (ASP-DAC, 2005)

Efficient Solution of Language Equations Using Partitioned Representations. - Alan Mishchenko; Robert K. Brayton; Jie-Hong Roland Jiang; Tiziano Villa; Nina Yevtushenko 001 (DATE, 2005)

Idle Speed control - a Benchmark for Hybrid System Research1. - Andrea Balluchi; Luca Benvenuti; Maria Domenica Di Benedetto; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (ADHS, 2006)

Efficient minimization of fully testable 2-SPP networks. - Anna Bernasconi 001; Valentina Ciriani; Rolf Drechsler; Tiziano Villa (DATE, 2006)

Complexity of two-level logic minimization. - Christopher Umans; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

A new algorithm for the largest compositionally progressive solution of synchronous language equations. - Tiziano Villa; Svetlana Zharikova; Nina Yevtushenko 001; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (ACM Great Lakes Symposium on VLSI, 2007)

FSM Encoding for BDD Representations. - Wilsin Gosti; Tiziano Villa; Alexander Saldanha; Alberto L. Sangiovanni-Vincentelli (Int. J. Appl. Math. Comput. Sci., 2007)

Compositionally Progressive Solutions of Synchronous FSM Equations. - Nina Yevtushenko 001; Tiziano Villa; Robert K. Brayton; Alexandre Petrenko; Alberto L. Sangiovanni-Vincentelli (Discret. Event Dyn. Syst., 2008)

Logic Minimization and Testability of 2-SPP Networks. - Anna Bernasconi 001; Valentina Ciriani; Rolf Drechsler; Tiziano Villa (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

An FSM Reengineering Approach to Sequential Circuit Synthesis by State Splitting. - Lin Yuan; Gang Qu 001; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

On decomposing Boolean functions via extended cofactoring. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (DATE, 2009)

The impact of EFSM composition on functional ATPG. - Davide Bresolin; Giuseppe Di Guglielmo; Franco Fummi; Graziano Pravadelli; Tiziano Villa (DDECS, 2009)

Logic Minimization and Testability of 2SPP-P-Circuits. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (DSD, 2009)

Discussion on Supervisory Control by Solving Automata Equation - Victor Bushkov; Nina Yevtushenko 001; Tiziano Villa (CoRR, 2009)

Hardware Equivalence and Property Verification. - Jie-Hong Roland Jiang; Tiziano Villa; Yves Crama; Peter L. Hammer (Boolean Models and Methods, 2010)

Synthesis of Multilevel Boolean Networks. - Tiziano Villa; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli; Yves Crama; Peter L. Hammer (Boolean Models and Methods, 2010)

An approximation algorithm for cofactoring-based synthesis. - Anna Bernasconi 001; Valentina Ciriani; Valentino Liberali; Gabriella Trucco; Tiziano Villa (ACM Great Lakes Symposium on VLSI, 2011)

Correct-by-construction code generation from hybrid automata specification. - Davide Bresolin; Luigi Di Guglielmo; Luca Geretti; Tiziano Villa (IWCMC, 2011)

Robotic Surgery. - Riccardo Muradore; Davide Bresolin; Luca Geretti; Paolo Fiorini; Tiziano Villa (IEEE Robotics Autom. Mag., 2011)

Computing the Evolution of Hybrid Systems using Rigorous Function Calculus. - Pieter Collins; Davide Bresolin; Luca Geretti; Tiziano Villa (ADHS, 2012)

Projected Don't Cares. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (DSD, 2012)

Open Problems in Verification and Refinement of Autonomous Robotic Systems. - Davide Bresolin; Luigi Di Guglielmo; Luca Geretti; Riccardo Muradore; Paolo Fiorini; Tiziano Villa (DSD, 2012)

Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis. - Luca Benvenuti; Davide Bresolin; Pieter Collins; Alberto Ferrari; Luca Geretti; Tiziano Villa (RP, 2012)

Synthesis of P-circuits for logic restructuring. - Anna Bernasconi 001; Valentina Ciriani; Valentino Liberali; Gabriella Trucco; Tiziano Villa (Integr., 2012)

Minimization of P-circuits using Boolean relations. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (DATE, 2013)

Synthesis of Implementable Control Strategies for Lazy Linear Hybrid Automata. - Luigi Di Guglielmo; Sanjit A. Seshia; Tiziano Villa (FedCSIS, 2013)

Minimization of EP-SOPs via Boolean relations. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (VLSI-SoC, 2013)

SOP restructuring by exploiting don't cares. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (Microprocess. Microsystems, 2013)

Verification of Robotic Surgery Tasks by Reachability Analysis: A Comparison of Tools. - Davide Bresolin; Luca Geretti; Riccardo Muradore; Paolo Fiorini; Tiziano Villa (DSD, 2014)

Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power. - Davide Bresolin; Khaled El-Fakih; Tiziano Villa; Nina Yevtushenko 001 (GandALF, 2014)

Bi-Decomposition Using Boolean Relations. - Anna Bernasconi 001; Robert K. Brayton; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (DSD, 2015)

Automated Synthesis of Protocol Converters with BALM-II. - Giovanni Castagnetti; Matteo Piccolo; Tiziano Villa; Nina Yevtushenko 001; Robert K. Brayton; Alan Mishchenko (SEFM Workshops, 2015)

Deriving Compositionally Deadlock-Free Components over Synchronous Automata Compositions. - Nina Yevtushenko 001; Khaled El-Fakih; Tiziano Villa; Jie-Hong R. Jiang (Comput. J., 2015)

Games, Automata, Logics, and Formal Verification (GandALF 2013). - Angelo Montanari; Gabriele Puppis; Tiziano Villa (Inf. Comput., 2015)

Formal verification of robotic surgery tasks by reachability analysis. - Davide Bresolin; Luca Geretti; Riccardo Muradore; Paolo Fiorini; Tiziano Villa (Microprocess. Microsystems, 2015)

Design Automation of Electronic Systems: Past Accomplishments and Challenges Ahead [Scanning the Issue]. - Robert K. Brayton; Luca P. Carloni; Alberto L. Sangiovanni-Vincentelli; Tiziano Villa (Proc. IEEE, 2015)

A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems. - Pierluigi Nuzzo 002; Alberto L. Sangiovanni-Vincentelli; Davide Bresolin; Luca Geretti; Tiziano Villa (Proc. IEEE, 2015)

Component-Based Design by Solving Language Equations. - Tiziano Villa; Alexandre Petrenko; Nina Yevtushenko 001; Alan Mishchenko; Robert K. Brayton (Proc. IEEE, 2015)

Using Flexibility in P-Circuits by Boolean Relations. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (IEEE Trans. Computers, 2015)

Logic Synthesis for Switching Lattices by Decomposition with P-Circuits. - Anna Bernasconi 001; Valentina Ciriani; Luca Frontini; Valentino Liberali; Gabriella Trucco; Tiziano Villa (DSD, 2016)

Ongoing Work on Automated Verification of Noisy Nonlinear Systems with Ariadne. - Luca Geretti; Davide Bresolin; Pieter Collins; Sanja Zivanovic Gonzalez; Tiziano Villa (ICTSS, 2017)

Hardware realization of residue number system algorithms by Boolean functions minimization. - Danila A. Gorodecky; Tiziano Villa (CoRR, 2018)

Enhancing logic synthesis of switching lattices by generalized Shannon decomposition methods. - Anna Bernasconi 001; Valentina Ciriani; Luca Frontini; Valentino Liberali; Gabriella Trucco; Tiziano Villa (Microprocess. Microsystems, 2018)

Formal Verification of Medical CPS: A Laser Incision Case Study. - Andre A. Geraldes; Luca Geretti; Davide Bresolin; Riccardo Muradore; Paolo Fiorini; Leonardo S. Mattos; Tiziano Villa (ACM Trans. Cyber Phys. Syst., 2018)

Automated Verification of Noisy Nonlinear Cyber-Physical Systems with Ariadne. - Davide Bresolin; Luca Geretti; Tiziano Villa (OVERLAY@AI*IA, 2019)

Strong Controllability of Temporal Networks with Decisions. - Matteo Zavatteri; Romeo Rizzi; Tiziano Villa (OVERLAY@AI*IA, 2019)

Complexity of Weak, Strong and Dynamic Controllability of CNCUs. - Matteo Zavatteri; Romeo Rizzi; Tiziano Villa (OVERLAY@AI*IA, 2019)

Efficient Implementation of Modular Division by Input Bit Splitting. - Danila A. Gorodecky; Tiziano Villa (ARITH, 2019)

Rigorous Continuous Evolution of Uncertain Systems. - Luca Geretti; Sanja Zivanovic Gonzalez; Pieter Collins; Davide Bresolin; Tiziano Villa (NSV@CAV, 2019)

Approximate Logic Synthesis by Symmetrization. - Anna Bernasconi 001; Valentina Ciriani; Tiziano Villa (DATE, 2019)

Boolean Minimization of Projected Sums of Products via Boolean Relations. - Anna Bernasconi 001; Valentina Ciriani; Gabriella Trucco; Tiziano Villa (IEEE Trans. Computers, 2019)

Dynamic Controllability and (J, K)-Resiliency in Generalized Constraint Networks with Uncertainty. - Matteo Zavatteri; Romeo Rizzi; Tiziano Villa (ICAPS, 2020)

On the Complexity of Resource Controllability in Business Process Management. - Matteo Zavatteri; Romeo Rizzi; Tiziano Villa (Business Process Management Workshops, 2020)

Computing the full quotient in bi-decomposition by approximation. - Anna Bernasconi 001; Valentina Ciriani; Jordi Cortadella; Tiziano Villa (DATE, 2020)

A computable and compositional semantics for hybrid automata. - Davide Bresolin; Pieter Collins; Luca Geretti; Roberto Segala; Tiziano Villa; Sanja Zivanovic Gonzalez (HSCC, 2020)

Mining Significant Temporal Networks Is Polynomial. - Guido Sciavicco; Matteo Zavatteri; Tiziano Villa (TIME, 2020)

Higher Order Method for Differential Inclusions. - Sanja Zivanovic Gonzalez; Pieter Collins; Luca Geretti; Davide Bresolin; Tiziano Villa (CoRR, 2020)

The Quotient in Preorder Theories. - Íñigo X. Íncer Romeo; Leonardo Mangeruca; Tiziano Villa; Alberto L. Sangiovanni-Vincentelli (GandALF, 2020)

A Boolean Heuristic for Disjoint SOP Synthesis. - Padmanabhan Balasubramanian; Anna Bernasconi 001; Valentina Ciriani; Tiziano Villa (DSD, 2021)

Decomposition of transition systems into sets of synchronizing state machines. - Viktor Teren; Jordi Cortadella; Tiziano Villa (DSD, 2021)

Mining Temporal Networks: Results and Open Problems. - Guido Sciavicco; Tiziano Villa; Matteo Zavatteri (OVERLAY@GandALF, 2021)

Equivalence checking and intersection of deterministic timed finite state machines. - Davide Bresolin; Khaled El-Fakih; Tiziano Villa; Nina Yevtushenko 001 (Formal Methods Syst. Des., 2021)

Mining CSTNUDs significant for a set of traces is polynomial. - Guido Sciavicco; Matteo Zavatteri; Tiziano Villa (Inf. Comput., 2021)

Dynamic Controllability of Temporal Networks via Supervisory Control. - Matteo Zavatteri; Davide Bresolin; Romeo Rizzi; Tiziano Villa (OVERLAY@AI*IA, 2022)

Decomposition of transition systems into sets of synchronizing Free-choice Petri Nets. - Viktor Teren; Jordi Cortadella; Tiziano Villa (DSD, 2022)

Process-driven Collision Prediction in Human-Robot Work Environments. - Luca Geretti; Stefano Centomo; Michele Boldo; Enrico Martini; Nicola Bombieri; Davide Quaglia; Tiziano Villa (ETFA, 2022)

Automating Numerical Parameters Along the Evolution of a Nonlinear System. - Luca Geretti; Pieter Collins; Davide Bresolin; Tiziano Villa (RV, 2022)

Special issue: Formal verification of cyber-physical systems. - Luca Geretti; Alessandro Abate; Pierluigi Nuzzo 002; Tiziano Villa (Inf. Comput., 2022)

Dynamic controllability of temporal networks with instantaneous reaction. - Matteo Zavatteri; Romeo Rizzi; Tiziano Villa (Inf. Sci., 2022)

Exploiting Symmetrization and D-Reducibility for Approximate Logic Synthesis. - Anna Bernasconi 001; Valentina Ciriani; Tiziano Villa (IEEE Trans. Computers, 2022)

HermesBDD: A Multi-Core and Multi-Platform Binary Decision Diagram Package. - Luigi Capogrosso; Luca Geretti; Marco Cristani; Franco Fummi; Tiziano Villa (DDECS, 2023)

Seto: A Framework for the Decomposition of Petri Nets and Transition Systems. - Viktor Teren; Jordi Cortadella; Tiziano Villa (DSD, 2023)

Generation of synchronizing state machines from a transition system: A region-based approach. - Viktor Teren; Jordi Cortadella; Tiziano Villa (Int. J. Appl. Math. Comput. Sci., 2023)

Dependability Evaluation of Industrial Networks by Using Monte Carlo With Importance Sampling. - Paolo Guarino; Filippo Nevi; Paolo Dai Pra; Davide Quaglia; Tiziano Villa (ETFA, 2024)

Recent Results on Computable and Compositional Semantics for Hybrid Systems. - Davide Bresolin; Pieter Collins; Luca Geretti; Roberto Segala; Tiziano Villa (OVERLAY, 2024)

Enhancing Safety and Privacy in Industry 4.0: The ICE Laboratory Case Study. - Federico Cunico; Stefano Aldegheri; Andrea Avogaro; Michele Boldo; Nicola Bombieri; Luigi Capogrosso; Ariel Caputo; Damiano Carra; Stefano Centomo; Dong Seon Cheng; Ettore Cinquetti; Marco Cristani; et al. (IEEE Access, 2024)

A computable and compositional semantics for hybrid systems. - Davide Bresolin; Pieter Collins; Luca Geretti; Roberto Segala; Tiziano Villa; Sanja Zivanovic Gonzalez (Inf. Comput., 2024)

Rigorous Function Calculi in Ariadne. - Pieter Collins; Luca Geretti; Sanja Zivanovic Gonzalez; Davide Bresolin; Tiziano Villa (Log. Methods Comput. Sci., 2025)

Area-driven Boolean bi-decomposition by function approximation. - Anna Bernasconi 001; Valentina Ciriani; Jordi Cortadella; Marco Costa; Tiziano Villa (ACM Trans. Design Autom. Electr. Syst., 2025)