Travelled to:
1 × Estonia
1 × Hungary
1 × Turkey
1 × United Kingdom
2 × Canada
2 × Denmark
2 × Italy
22 × USA
3 × France
3 × Germany
Collaborated with:
L.Zhang M.Martonosi P.Ashar Y.Yu W.Qin Y.S.Li D.Tang K.Keutzer Z.Fu S.Devadas Z.Huang A.Gupta Y.Zhao Y.Yetim Y.Vizel S.Rajagopalan G.Araujo B.Çakir C.S.Zhu D.Schwartz-Narbonne ∅ X.Zhu D.Ranjan H.Jyu P.Subramanyan A.Gurfinkel G.Weissenbacher D.Kröning K.Chen P.Patra H.Wang L.Peh Y.S.Mahajan S.Wang R.A.Bergamaschi F.Xie S.Ghosh M.T.Lee V.Tiwari A.Saldanha F.Liu D.I.August C.Chan D.Sethi C.N.Ip P.Zhong A.R.Wang M.K.Ganai G.Ottoni S.Rigo M.W.Moskewicz C.F.Madigan W.Yang N.Tsiskaridze K.Pasricha D.Reisman A.Susnea M.Sgroi M.Sheets A.Mihal J.M.Rabaey A.L.Sangiovanni-Vincentelli G.Smith D.Nadamuni R.Chapman J.Fogelin G.Martin B.Bailey Mark Gallagher Lauren Biernacki Shibo Chen Zelalem Birhanu Aweke Salessawi Ferede Yitbarek Misiker Tadesse Aga A.Harris Zhixing Xu B.Kasikci V.Bertacco M.Tiwari T.M.Austin
Talks about:
use (13) base (11) circuit (8) analysi (7) solver (7) sat (7) satisfi (6) boolean (6) effici (6) embed (6)
Person: Sharad Malik
DBLP: Malik:Sharad
Facilitated 2 volumes:
Contributed to:
Wrote 54 papers:
- ASPLOS-2015-YetimMM #communication #execution #fault #named #parallel
- CommGuard: Mitigating Communication Errors in Error-Prone Parallel Execution (YY, SM, MM), pp. 311–323.
- CAV-2015-VizelGM #performance
- Fast Interpolating BMC (YV, AG, SM), pp. 641–657.
- DATE-2015-CakirM #clustering #correlation #detection #hardware #using
- Hardware Trojan detection for gate-level ICs using signal correlation based clustering (BÇ, SM), pp. 471–476.
- DATE-2015-ZhuM #linear #machine learning #optimisation #programming #using
- Optimizing dynamic trace signal selection using machine learning and linear programming (CSZ, SM), pp. 1289–1292.
- DATE-2013-SubramanyanTPRSM #analysis #functional #reverse engineering #using
- Reverse engineering digital circuits using functional analysis (PS, NT, KP, DR, AS, SM), pp. 1277–1280.
- DATE-2013-YetimMM #streaming
- Extracting useful computation from error-prone processors for streaming applications (YY, MM, SM), pp. 202–207.
- CAV-2012-Schwartz-NarbonneLAM #debugging #named #parallel #source code
- passert: A Tool for Debugging Parallel Programs (DSN, FL, DIA, SM), pp. 751–757.
- DAC-2012-ChanSSM #hardware #specification #synthesis
- Specification and synthesis of hardware checkpointing and rollback mechanisms (CC, DSN, DS, SM), pp. 1226–1232.
- TACAS-2012-WeissenbacherKM #contest #debugging #named
- Wolverine: Battling Bugs with Interpolants — (Competition Contribution) (GW, DK, SM), pp. 556–558.
- HPCA-2008-ChenMP #constraints #graph #memory management #runtime #using #validation
- Runtime validation of memory ordering using constraint graph checking (KC, SM, PP), pp. 415–426.
- TACAS-2008-Malik #hardware #verification
- Hardware Verification: Techniques, Methodology and Solutions (SM), p. 1.
- SAT-2006-FuM #on the #problem #satisfiability
- On Solving the Partial MAX-SAT Problem (ZF, SM), pp. 252–265.
- SAT-2006-TangM #quantifier
- Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares (DT, SM), pp. 368–381.
- SAT-2006-YuM #constraints #learning #linear #smt
- Lemma Learning in SMT on Linear Constraints (YY, SM), pp. 142–155.
- CAV-2005-TangMGI #model checking #reduction #satisfiability #symmetry
- Symmetry Reduction in SAT-Based Model Checking (DT, SM, AG, CNI), pp. 125–138.
- DATE-2005-FuYM #satisfiability
- Considering Circuit Observability Don’t Cares in CNF Satisfiability (ZF, YY, SM), pp. 1108–1113.
- DATE-2005-WangPM #energy #network
- A Technology-Aware and Energy-Oriented Topology Exploration for On-Chip Networks (HW, LSP, SM), pp. 1238–1243.
- DATE-v2-2004-ZhuM #architecture #communication #framework #multi #prototype #specification #using
- Using a Communication Architecture Specification in an Application-Driven Retargetable Prototyping Platform for Multiprocessing (XZ, SM), pp. 1244–1249.
- LCTES-2004-QinRM #architecture #concurrent #development #modelling #synthesis #tool support
- A formal concurrency model based architecture description language for synthesis of software development tools (WQ, SR, SM), pp. 47–56.
- SAT-2004-TangYRM #algorithm #analysis #problem #quantifier #satisfiability
- Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems (DT, YY, DR, SM), pp. 214–223.
- SAT-J-2004-MahajanFM05 #named #performance #satisfiability
- Zchaff2004: An Efficient SAT Solver (YSM, ZF, SM), pp. 360–375.
- SAT-J-2004-TangYRM05 #algorithm #analysis #problem #quantifier #satisfiability
- Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems (DT, YY, DR, SM), pp. 292–305.
- DAC-2003-QinM #automation #performance #synthesis
- Automated synthesis of efficient binary decoders for retargetable software toolkits (WQ, SM), pp. 764–769.
- DATE-2003-QinM #flexibility #formal method #modelling #simulation
- Flexible and Formal Modeling of Microprocessors with Application to Retargetable Simulation (WQ, SM), pp. 10556–10561.
- DATE-2003-WangMB #embedded #integration #modelling
- Modeling and Integration of Peripheral Devices in Embedded Systems (SW, SM, RAB), pp. 10136–10141.
- DATE-2003-ZhangM #implementation #independence #satisfiability #using #validation
- Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications (LZ, SM), pp. 10880–10885.
- PLDI-2003-XieMM #scalability
- Compile-time dynamic voltage scaling settings: opportunities and limits (FX, MM, SM), pp. 49–62.
- SAT-2003-ZhangM #algorithm #case study #implementation #performance #satisfiability
- Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms (LZ, SM), pp. 287–298.
- CADE-2002-ZhangM #performance #satisfiability
- The Quest for Efficient Boolean Satisfiability Solvers (LZ, SM), pp. 295–313.
- CAV-2002-ZhangM #performance #satisfiability
- The Quest for Efficient Boolean Satisfiability Solvers (LZ, SM), pp. 17–36.
- DAC-2002-GanaiAGZM #algorithm #satisfiability
- Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver (MKG, PA, AG, LZ, SM), pp. 747–750.
- DAC-2002-HuangM #configuration management #parallel
- Exploiting operation level parallelism through dynamically reconfigurable datapaths (ZH, SM), pp. 337–342.
- DAC-2002-SmithNMCFKMB #embedded #question #tool support
- Unified tools for SoC embedded systems: mission critical, mission impossible or mission irrelevant? (GS, DN, SM, RC, JF, KK, GM, BB), p. 479.
- CC-2001-OttoniRARM #embedded #source code
- Optimal Live Range Merge for Address Register Allocation in Embedded Programs (GO, SR, GA, SR, SM), pp. 274–288.
- DAC-2001-MoskewiczMZZM #named #performance #satisfiability
- Chaff: Engineering an Efficient SAT Solver (MWM, CFM, YZ, LZ, SM), pp. 530–535.
- DAC-2001-SgroiSMKMRS #design
- Addressing the System-on-a-Chip Interconnect Woes Through Communication-Based Design (MS, MS, AM, KK, SM, JMR, ALSV), pp. 667–672.
- DATE-2001-HuangM #configuration management #design #network #using
- Managing dynamic reconfiguration overhead in systems-on-a-chip design using reconfigurable datapaths and optimized interconnection networks (ZH, SM), p. 735.
- DAC-1999-ZhaoM #array #estimation #memory management
- Exact Memory Size Estimation for Array Computations without Loop Unrolling (YZ, SM), pp. 811–816.
- ASPLOS-1998-GhoshMM #analysis #precise #program transformation
- Precise Miss Analysis for Program Transformations with Caches of Arbitrary Associativity (SG, MM, SM), pp. 228–239.
- DAC-1998-ZhongAMM #case study #configuration management #problem #satisfiability #using
- Using Reconfigurable Computing Techniques to Accelerate Problems in the CAD Domain: A Case Study with Boolean Satisfiability (PZ, PA, SM, MM), pp. 194–199.
- DAC-1997-GuptaMA #formal method #simulation #towards #using #validation
- Toward Formalizing a Validation Methodology Using Simulation Coverage (AG, SM, PA), pp. 740–745.
- DAC-1997-MalikML #analysis #embedded
- Static Timing Analysis of Embedded Software (SM, MM, YTSL), pp. 147–152.
- DAC-1996-AraujoML #architecture #code generation #using
- Using Register-Transfer Paths in Code Generation for Heterogeneous Memory-Register Architectures (GA, SM, MTCL), pp. 591–596.
- DAC-1995-DevadasM #optimisation #overview #power management
- A Survey of Optimization Techniques Targeting Low Power VLSI Circuits (SD, SM), pp. 242–247.
- DAC-1995-LiM #analysis #embedded #performance #using
- Performance Analysis of Embedded Software Using Implicit Path Enumeration (YTSL, SM), pp. 456–461.
- LCT-RTS-1995-LiM #analysis #embedded #performance #using
- Performance Analysis of Embedded Software Using Implicit Path Enumeration (YTSL, SM), pp. 88–98.
- DAC-1994-AsharM #low cost #set
- Implicit Computation of Minimum-Cost Feedback-Vertex Sets for Partial Scan and Other Applications (PA, SM), pp. 77–80.
- DAC-1994-JyuM #design #logic #modelling #statistics #synthesis
- Statistical Delay Modeling in Logic Design and Synthesis (HFJ, SM), pp. 126–130.
- DAC-1993-TiwariAM
- Technology Mapping for Lower Power (VT, PA, SM), pp. 74–79.
- DAC-1992-DevadasKMW #logic #verification
- Certified Timing Verification and the Transition Delay of a Logic Circuit (SD, KK, SM, ARW), pp. 549–555.
- DAC-1991-DevadasKM #algorithm #generative #multi #testing
- A Synthesis-Based Test Generation and Compaction Algorithm for Multifaults (SD, KK, SM), pp. 359–365.
- DAC-1990-KeutzerMS
- Is Redundancy Necessary to Reduce Delay (KK, SM, AS), pp. 228–234.
- CAV-2018-YangVSGM #composition #lazy evaluation #security #self #verification
- Lazy Self-composition for Security Verification (WY, YV, PS, AG, SM), pp. 136–156.
- ASPLOS-2019-GallagherBCAYAH #architecture #named
- Morpheus: A Vulnerability-Tolerant Secure Architecture Based on Ensembles of Moving Target Defenses with Churn (MG, LB, SC, ZBA, SFY, MTA, AH, ZX, BK, VB, SM, MT, TMA), pp. 469–484.