BU | CMPE

Bogazici University

 

Alper Şen

Site menu:

|  |  Research||Opportunities || PublicationsTeachingProfessionalContact | | 

 

 


Opportunities

Job Opportunities

There is a contract position in IBM Austin for applied sequential equivalence checking with possibly some other formal verification tasks using IBM's SixthSense tool. Depending on the skill of the candidate, this could include some interesting methodology / tool work, and could evolve into a permanent position. Candidates should have related experience, HDL and logic design familiarity, ideally some familiarity with verification / equivalence checking, some coding/scripting experience.
Contact me ASAP. Posted October 5, 2010

Research Opportunities

I am looking for motivated MS and PhD students to work on projects some of which are listed below. Funding is available.

Verification is the general research area that many of these projects are centered around. Verification consumes 60-70% of the overall software or hardware design cycle, hence it is a very costly process. The verification problem is growing with the introduction of multi-threaded, concurrent software and multiple processor systems. Software, hardware, telecommunication, semiconductor companies such as Microsoft, Google, Intel, Freescale, IBM, ST Micro, Siemens are all interested in verification solutions. Our goal is to develop efficient and industrial scale solutions to the verification problem.

Predictive Verification of Concurrent, Multithreaded Systems

In this project, the goal is to develop analysis techniques to increase reliability of concurrent hardware and software systems. In particular, we propose to enhance and further develop our predictive verification techniques that preserve concurrency information and exploit it to find both actual and potential bugs. Automated tools will be implemented to validate the effectiveness of the approach. System level programming languages such as SystemC will be used.

Multicore Programming of Design Automation Algorithms

Multicore programming has been a reality with the emergence of recent hardware from companies such as Intel, AMD, Freescale, NVIDIA. In particular, graphical processing units (GPU) are equipped with hundreds of small cores enabling to execute 10,000 threads concurrently. New languages and standards such as OpenCL, CUDA, OpenMP are emerging as common platforms for multicore programming. The goal of this project is to port design automation algorithms such as simulation/verification algorithms into multicores resulting in big performance gains.

Mutation Analysis to Increase Verification Coverage

Mutation analysis is a popular technique in software testing that allows to increase coverage of tests. Recently a similar approach has been taken for hardware. Given a design/code and its tests/testbenches, in this project, the goal is first to define a set of mutations for the SystemC language. Second, to build an automated environment that inserts these mutations in the code. Third, to execute/simulate code and observe whether the given set of tests can detect these mutations at the outputs of the design. This work enables us to increase quality of verification tests.

Concoling Testing for SystemC

The idea of concolic testing is to use the symbolic (using symbols for variables) execution to generate inputs that direct a program to alternate executions, and to use the concrete (using actual values for variables) execution to guide the symbolic execution along a concrete path. Constrainst are generated during symbolic path generation. Symbolic values (variables) are replaced by concrete values if the symbolic state is too complex to be handled by a constraint path solver. The goal in this project is to extend concolic testing to the system level language SystemC in order to improve verification of code written in SystemC. Automated tools will be implemented to validate the effectiveness of the approach.

Tool Development

We previously developed Partial Order Trace Analyzer (POTA) tool for Java programs on Linux. In this project, the goal is to develop a modular code base allowing to plug in new verification algorithms and developing scripts and a GUI frontend.

Related Conferences:

  • Design Automation Conference (DAC)
  • Design Automation and Test in Europe (DATE)
  • Computer Aided Verification (CAV)
  • Formal Methods in Computer Aided Verification (FMCAD)
  • International Conference on CAD (ICCAD)
  • Microprocessor Test and Verification Workshop (MTV)
  • Automated Software Engineering (ASE)
  • International Parallel and Distributed Processing Symposium (IPDPS)
  • International Workshop on Formal Approaches to Testing of Software (FATES)
  • SPIN International Workshop
  • International Workshop on Runtime Verification (RV)
  • International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)
  • IEEE International High-Level Design Validation and Test Workshop (HLDVT)


    • Email Alper Sen.