A Verification Strategy for Timing-Constrained Systems. - Felice Balarin; Alberto L. Sangiovanni-Vincentelli (CAV, 1992)

An Iterative Approach to Language Containment. - Felice Balarin; Alberto L. Sangiovanni-Vincentelli (CAV, 1993)

Verilog HDL Modeling Styles for Formal Verification. - Felice Balarin; Gary York (CHDL, 1993)

On the Automatic Computation of Network Invariants. - Felice Balarin; Alberto L. Sangiovanni-Vincentelli (CAV, 1994)

HSIS: A BDD-Based Environment for Formal Verification. - Adnan Aziz; Felice Balarin; Szu-Tsung Cheng; Ramin Hojati; Timothy Kam; Sriram C. Krishnan; Rajeev K. Ranjan 001; Thomas R. Shiple; Vigyan Singhal; Serdar Tasiran; Huey-Yih Wang; Robert K. Brayton; et al. (DAC, 1994)

Iterative algorithms for formal verification of embedded real-time systems. - Felice Balarin; Alberto L. Sangiovanni-Vincentelli (ICCAD, 1994)

Supervisory Control of Finite State Machines. - Adnan Aziz; Felice Balarin; Robert K. Brayton; Marika Domenica Di Benedetto; Alexander Saldanha (CAV, 1995)

It Usually Works: The Temporal Logic of Stochastic Systems. - Adnan Aziz; Vigyan Singhal; Felice Balarin (CAV, 1995)

An Iterative Approach to Verification of Real-Time Systems. - Felice Balarin; Alberto L. Sangiovanni-Vincentelli (Formal Methods Syst. Des., 1995)

Formal Verification of Embedded Systems based on CFSM Networks. - Felice Balarin; Harry Hsieh; Attila Jurecska; Luciano Lavagno; Alberto L. Sangiovanni-Vincentelli (DAC, 1996)

Approximate reachability analysis of timed automata. - Felice Balarin (RTSS, 1996)

Automatic Generation of a Real-Time Operating System for Embedded Systems. - Felice Balarin; Massimiliano Chiodo; Attila Jurecska; Luciano Lavagno; Bassam Tabbara; Alberto L. Sangiovanni-Vincentelli (CODES, 1997)

Schedule Validation for Embedded Reactive Real-Time Systems. - Felice Balarin; Alberto L. Sangiovanni-Vincentelli (DAC, 1997)

Verifying invariants by approximate image computation. - Felice Balarin (INFINITY, 1997)

Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models. - Felice Balarin (CAV, 1998)

Priority Assignment for Embedded Reactive Real-Time Systems. - Felice Balarin (LCTES, 1998)

Scheduling for Embedded Real-Time Systems. - Felice Balarin; Luciano Lavagno; Praveen K. Murthy; Alberto L. Sangiovanni-Vincentelli (IEEE Des. Test Comput., 1998)

Worst-case analysis of discrete systems based on conditional abstractions. - Felice Balarin (CODES, 1999)

Worst-case analysis of discrete systems. - Felice Balarin (ICCAD, 1999)

Synchronous equivalence for embedded systems: a tool for design exploration. - Harry Hsieh; Felice Balarin (ICCAD, 1999)

Software Synthesis for Complex Reactive Embedded Systems. - Felice Balarin; Massimiliano Chiodo (ICCD, 1999)

Equivalences for Fair Kripke Structures. - Adnan Aziz; Felice Balarin; Vigyan Singhal; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (Chic. J. Theor. Comput. Sci., 1999)

Concurrent Symbolic Verification of Liveness Properties for Interleaved Models. - Felice Balarin (SMC@FLoC, 1999)

Synthesis of software programs for embedded control applications. - Felice Balarin; Massimiliano Chiodo; Paolo Giusto; Harry Hsieh; Attila Jurecska; Luciano Lavagno; Alberto L. Sangiovanni-Vincentelli; Ellen Sentovich; Kei Suzuki (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

Efficient methods for embedded system design space exploration. - Harry Hsieh; Felice Balarin; Luciano Lavagno; Alberto L. Sangiovanni-Vincentelli (DAC, 2000)

Task scheduling with RT constraints. - Marco Di Natale; Alberto L. Sangiovanni-Vincentelli; Felice Balarin (DAC, 2000)

Automatic Abstraction for Worst-Case Analysis of Discrete Systems. - Felice Balarin (DATE, 2000)

Refining abstract equivalence analysis for embedded system design. - Harry Hsieh; Felice Balarin (HLDVT, 2000)

Sequential synthesis using S1S. - Adnan Aziz; Felice Balarin; Robert K. Brayton; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000)

STARS of MPEG decoder: a case study in worst-case analysis of discrete-event systems. - Felice Balarin (CODES, 2001)

Constraints specification at higher levels of abstraction. - Felice Balarin; Jerry R. Burch; Luciano Lavagno; Yosinori Watanabe; Roberto Passerone; Alberto L. Sangiovanni-Vincentelli (HLDVT, 2001)

Stars in VCC: Complementing Simulation with Worst-Case Analysis. - Felice Balarin (ICCAD, 2001)

Scheduling Reactive Task Graphs in Embedded Control Systems. - Marco Di Natale; Alberto L. Sangiovanni-Vincentelli; Felice Balarin (IEEE Real Time Technology and Applications Symposium, 2001)

Synchronous approach to the functional equivalence of embeddedsystem implementations. - Harry Hsieh; Felice Balarin; Luciano Lavagno; Alberto L. Sangiovanni-Vincentelli (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001)

Modeling and Designing Heterogeneous Systems. - Felice Balarin; Luciano Lavagno; Claudio Passerone; Alberto L. Sangiovanni-Vincentelli; Marco Sgroi; Yosinori Watanabe (Concurrency and Hardware Design, 2002)

Concurrent execution semantics and sequential simulation algorithms for the metropolis meta-model. - Felice Balarin; Luciano Lavagno; Claudio Passerone; Alberto L. Sangiovanni-Vincentelli; Yosinori Watanabe; Guang Yang 004 (CODES, 2002)

Processes, Interfaces and Platforms. Embedded Software Modeling in Metropolis. - Felice Balarin; Luciano Lavagno; Claudio Passerone; Yosinori Watanabe (EMSOFT, 2002)

Formal verification of embedded system designs at multiple levels of abstraction. - Xi Chen 024; Fang Chen; Harry Hsieh; Felice Balarin; Yosinori Watanabe (HLDVT, 2002)

Simulation Trace Verification for Quantitative Constraints. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (Embedded Software for SoC, 2003)

Case Studies of Model Checking for Embedded System Designs. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (ACSD, 2003)

Automatic trace analysis for logic of constraints. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (DAC, 2003)

Automatic Generation of Simulation Monitors from Quantitative Constraint Formula. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (DATE, 2003)

Verifying LOC based functional and performance constraints. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (HLDVT, 2003)

Metropolis: An Integrated Electronic System Design Environment. - Felice Balarin; Yosinori Watanabe; Harry Hsieh; Luciano Lavagno; Claudio Passerone; Alberto L. Sangiovanni-Vincentelli (Computer, 2003)

Formal Verification for Embedded System Designs. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (Des. Autom. Embed. Syst., 2003)

Utilizing Formal Assertions for System Design of Network Processors. - Xi Chen 024; Yan Luo 001; Harry Hsieh; Laxmi N. Bhuyan; Felice Balarin (DATE, 2004)

Separation of concerns: overhead in modeling and efficient simulation techniques. - Guang Yang 004; Alberto L. Sangiovanni-Vincentelli; Yosinori Watanabe; Felice Balarin (EMSOFT, 2004)

Assertion-based power/performance analysis of network processor architectures. - Jia Yu 008; Wei Wu 024; Xi Chen 024; Harry Hsieh; Jun Yang 002; Felice Balarin (HLDVT, 2004)

Assertion Based Verification and Analysis of Network Processor Architectures. - Xi Chen 024; Yan Luo 001; Harry Hsieh; Laxmi N. Bhuyan; Felice Balarin (Des. Autom. Embed. Syst., 2004)

Logic of constraints: a quantitative performance and functional constraint formalism. - Xi Chen 024; Harry Hsieh; Felice Balarin; Yosinori Watanabe (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004)

Assertion-Based Design Exploration of DVS in Network Processor Architectures. - Jia Yu 008; Wei Wu 024; Xi Chen 024; Harry Hsieh; Jun Yang 002; Felice Balarin (DATE, 2005)

A formal approach to system level design: metamodels and unified design environments. - Felice Balarin; Roberto Passerone; Alessandro Pinto; Alberto L. Sangiovanni-Vincentelli (MEMOCODE, 2005)

Functional verification methodology based on formal interface specification and transactor generation. - Felice Balarin; Roberto Passerone (DATE, 2006)

Communication and co-simulation infrastructure for heterogeneous system integration. - Guang Yang 004; Xi Chen 024; Felice Balarin; Harry Hsieh; Alberto L. Sangiovanni-Vincentelli (DATE, 2006)

Verification Approach of Metropolis Design Framework for Embedded Systems. - Xi Chen 024; Harry Hsieh; Felice Balarin (Int. J. Parallel Program., 2006)

Framework for fast and accurate performance simulation of multiprocessor systems. - Eric Cheung; Harry Hsieh; Felice Balarin (HLDVT, 2007)

Automatic buffer sizing for rate-constrained KPN applications on multiprocessor system-on-chip. - Eric Cheung; Harry Hsieh; Felice Balarin (HLDVT, 2007)

Specification, Synthesis, and Simulation of Transactor Processes. - Felice Balarin; Roberto Passerone (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2007)

Software optimization for MPSoC: a mpeg-2 decoder case study. - Eric Cheung; Harry Hsieh; Felice Balarin (CODES+ISSS, 2008)

Partial order method for timed simulation of system-level MPSoC designs. - Eric Cheung; Harry Hsieh; Felice Balarin (ASP-DAC, 2009)

Fast and accurate performance simulation of embedded software for MPSoC. - Eric Cheung; Harry Hsieh; Felice Balarin (ASP-DAC, 2009)

Memory subsystem simulation in software TLM/T models. - Eric Cheung; Harry Hsieh; Felice Balarin (ASP-DAC, 2009)